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

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

Proof of Theorem an4
StepHypRef Expression
1 an12 561 . . 3 ((𝜓 ∧ (𝜒𝜃)) ↔ (𝜒 ∧ (𝜓𝜃)))
21anbi2i 457 . 2 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
3 anass 401 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒𝜃))))
4 anass 401 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
52, 3, 43bitr4i 212 1 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  an42  587  an4s  588  anandi  590  anandir  591  rnlem  976  an6  1321  2eu4  2119  reean  2645  reu2  2925  rmo4  2930  rmo3f  2934  rmo3  3054  inxp  4760  xp11m  5066  fununi  5283  fun  5387  resoprab2  5969  xporderlem  6229  poxp  6230  th3qlem1  6634  enq0enq  7427  enq0tr  7430  genpdisj  7519  cju  8914  elfzo2  10145  iooinsup  11278  summodc  11384  prodmodc  11579  issubmd  12797  dvdsrtr  13201  txbasval  13638  txcnp  13642  txlm  13650
  Copyright terms: Public domain W3C validator