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

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

Proof of Theorem an4
StepHypRef Expression
1 an12 483 . . 3 ((ψ (χ θ)) ↔ (χ (ψ θ)))
21anbi2i 433 . 2 ((φ (ψ (χ θ))) ↔ (φ (χ (ψ θ))))
3 anass 383 . 2 (((φ ψ) (χ θ)) ↔ (φ (ψ (χ θ))))
4 anass 383 . 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  508  an4s  509  anandi  511  anandir  512  rnlem  869  an6  1199  2eu4  1971  reean  2452  reu2  2702  rmo4  2707  rmo3  2822  inxp  4393  xp11m  4682  fununi  4889  fun  4984  resoprab2  5517  xporderlem  5770  poxp  5771  th3qlem1  6115  enq0enq  6280  enq0tr  6283  genpdisj  6372
  Copyright terms: Public domain W3C validator