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

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

Proof of Theorem an4
StepHypRef Expression
1 an12 495 . . 3 ((ψ (χ θ)) ↔ (χ (ψ θ)))
21anbi2i 430 . 2 ((φ (ψ (χ θ))) ↔ (φ (χ (ψ θ))))
3 anass 381 . 2 (((φ ψ) (χ θ)) ↔ (φ (ψ (χ θ))))
4 anass 381 . 2 (((φ χ) (ψ θ)) ↔ (φ (χ (ψ θ))))
52, 3, 43bitr4i 201 1 (((φ ψ) (χ θ)) ↔ ((φ χ) (ψ θ)))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  an42  521  an4s  522  anandi  524  anandir  525  rnlem  882  an6  1215  2eu4  1990  reean  2472  reu2  2723  rmo4  2728  rmo3  2843  inxp  4413  xp11m  4702  fununi  4910  fun  5006  resoprab2  5540  xporderlem  5793  poxp  5794  th3qlem1  6144  enq0enq  6413  enq0tr  6416  genpdisj  6505  cju  7674  elfzo2  8757
 Copyright terms: Public domain W3C validator