New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  an4 GIF version

Theorem an4 797
 Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
Assertion
Ref Expression
an4 (((φ ψ) (χ θ)) ↔ ((φ χ) (ψ θ)))

Proof of Theorem an4
StepHypRef Expression
1 an12 772 . . 3 ((ψ (χ θ)) ↔ (χ (ψ θ)))
21anbi2i 675 . 2 ((φ (ψ (χ θ))) ↔ (φ (χ (ψ θ))))
3 anass 630 . 2 (((φ ψ) (χ θ)) ↔ (φ (ψ (χ θ))))
4 anass 630 . 2 (((φ χ) (ψ θ)) ↔ (φ (χ (ψ θ))))
52, 3, 43bitr4i 268 1 (((φ ψ) (χ θ)) ↔ ((φ χ) (ψ θ)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358 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 177  df-an 360 This theorem is referenced by:  an42  798  an4s  799  anandi  801  anandir  802  rnlem  931  an6  1261  2eu1  2284  2eu4  2287  reean  2777  reu2  3024  rmo4  3029  rmo3  3133  inxpk  4277  dfpw12  4301  ltfintr  4459  opelxp  4811  inxp  4863  xp11  5056  fununi  5160  2elresin  5194  fun  5236  resoprab2  5582  brtxp  5783  qrpprod  5836  fundmen  6043
 Copyright terms: Public domain W3C validator