Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  an4 GIF version

Theorem an4 528
 Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
Assertion
Ref Expression
an4 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))

Proof of Theorem an4
StepHypRef Expression
1 an12 503 . . 3 ((𝜓 ∧ (𝜒𝜃)) ↔ (𝜒 ∧ (𝜓𝜃)))
21anbi2i 438 . 2 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
3 anass 387 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒𝜃))))
4 anass 387 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
52, 3, 43bitr4i 205 1 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))
 Colors of variables: wff set class Syntax hints:   ∧ wa 101   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  an42  529  an4s  530  anandi  532  anandir  533  rnlem  894  an6  1227  2eu4  2009  reean  2495  reu2  2751  rmo4  2756  rmo3  2876  inxp  4497  xp11m  4786  fununi  4994  fun  5090  resoprab2  5625  xporderlem  5879  poxp  5880  th3qlem1  6238  enq0enq  6586  enq0tr  6589  genpdisj  6678  cju  7988  elfzo2  9108
 Copyright terms: Public domain W3C validator