This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem an82ds

Description: Inference exchanging the last antecedent with the second one. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypothesis an82ds.1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) → 𝜌 )
Assertion an82ds ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜎 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜓 ) → 𝜌 )

Proof

Step Hyp Ref Expression
1 an82ds.1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) → 𝜌 )
2 an32 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜎 ) ↔ ( ( 𝜑 ∧ 𝜎 ) ∧ 𝜓 ) )
3 2 anbi1i ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜎 ) ∧ 𝜃 ) ↔ ( ( ( 𝜑 ∧ 𝜎 ) ∧ 𝜓 ) ∧ 𝜃 ) )
4 3 anbi1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜎 ) ∧ 𝜃 ) ∧ 𝜏 ) ↔ ( ( ( ( 𝜑 ∧ 𝜎 ) ∧ 𝜓 ) ∧ 𝜃 ) ∧ 𝜏 ) )
5 4 anbi1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜎 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ↔ ( ( ( ( ( 𝜑 ∧ 𝜎 ) ∧ 𝜓 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) )
6 5 anbi1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜎 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ↔ ( ( ( ( ( ( 𝜑 ∧ 𝜎 ) ∧ 𝜓 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) )
7 1 an72ds ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜎 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜒 ) → 𝜌 )
8 6 7 sylanbr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜎 ) ∧ 𝜓 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜒 ) → 𝜌 )
9 8 an72ds ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜎 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜓 ) → 𝜌 )