Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  4an21 Structured version   Visualization version   GIF version

Theorem 4an21 43869
 Description: Rearrangement of 4 conjuncts with a triple conjunction. (Contributed by AV, 4-Mar-2022.)
Assertion
Ref Expression
4an21 (((𝜑𝜓) ∧ 𝜒𝜃) ↔ (𝜓 ∧ (𝜑𝜒𝜃)))

Proof of Theorem 4an21
StepHypRef Expression
1 3anass 1092 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) ↔ ((𝜑𝜓) ∧ (𝜒𝜃)))
2 ancom 464 . . . 4 ((𝜑𝜓) ↔ (𝜓𝜑))
32anbi1i 626 . . 3 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜓𝜑) ∧ (𝜒𝜃)))
4 anass 472 . . . 4 (((𝜓𝜑) ∧ (𝜒𝜃)) ↔ (𝜓 ∧ (𝜑 ∧ (𝜒𝜃))))
5 3anass 1092 . . . . . 6 ((𝜑𝜒𝜃) ↔ (𝜑 ∧ (𝜒𝜃)))
65bicomi 227 . . . . 5 ((𝜑 ∧ (𝜒𝜃)) ↔ (𝜑𝜒𝜃))
76anbi2i 625 . . . 4 ((𝜓 ∧ (𝜑 ∧ (𝜒𝜃))) ↔ (𝜓 ∧ (𝜑𝜒𝜃)))
84, 7bitri 278 . . 3 (((𝜓𝜑) ∧ (𝜒𝜃)) ↔ (𝜓 ∧ (𝜑𝜒𝜃)))
93, 8bitri 278 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (𝜓 ∧ (𝜑𝜒𝜃)))
101, 9bitri 278 1 (((𝜑𝜓) ∧ 𝜒𝜃) ↔ (𝜓 ∧ (𝜑𝜒𝜃)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator