Metamath Proof Explorer


Theorem an43

Description: Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion an43 ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) ↔ ( ( 𝜑𝜃 ) ∧ ( 𝜓𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 an42 ( ( ( 𝜑𝜃 ) ∧ ( 𝜓𝜒 ) ) ↔ ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) )
2 1 bicomi ( ( ( 𝜑𝜓 ) ∧ ( 𝜒𝜃 ) ) ↔ ( ( 𝜑𝜃 ) ∧ ( 𝜓𝜒 ) ) )