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

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

Proof of Theorem an4
StepHypRef Expression
1 an12 533 . . 3 ((𝜓 ∧ (𝜒𝜃)) ↔ (𝜒 ∧ (𝜓𝜃)))
21anbi2i 450 . 2 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
3 anass 396 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒𝜃))))
4 anass 396 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓𝜃))))
52, 3, 43bitr4i 211 1 (((𝜑𝜓) ∧ (𝜒𝜃)) ↔ ((𝜑𝜒) ∧ (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  an42  559  an4s  560  anandi  562  anandir  563  rnlem  943  an6  1282  2eu4  2068  reean  2574  reu2  2843  rmo4  2848  rmo3f  2852  rmo3  2970  inxp  4641  xp11m  4945  fununi  5159  fun  5263  resoprab2  5834  xporderlem  6094  poxp  6095  th3qlem1  6497  enq0enq  7203  enq0tr  7206  genpdisj  7295  cju  8679  elfzo2  9878  iooinsup  10997  summodc  11103  txbasval  12342  txcnp  12346  txlm  12354
  Copyright terms: Public domain W3C validator