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

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

Proof of Theorem an4
StepHypRef Expression
1 an12 526 . . 3 ((𝜓 ∧ (𝜒𝜃)) ↔ (𝜒 ∧ (𝜓𝜃)))
21anbi2i 445 . 2 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
3 anass 393 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒𝜃))))
4 anass 393 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
52, 3, 43bitr4i 210 1 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  an42  552  an4s  553  anandi  555  anandir  556  rnlem  918  an6  1253  2eu4  2036  reean  2528  reu2  2791  rmo4  2796  rmo3  2916  inxp  4528  xp11m  4823  fununi  5035  fun  5132  resoprab2  5677  xporderlem  5931  poxp  5932  th3qlem1  6324  enq0enq  6893  enq0tr  6896  genpdisj  6985  cju  8315  elfzo2  9451
  Copyright terms: Public domain W3C validator