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

Theorem an32s 502
Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
Hypothesis
Ref Expression
an32s.1 (((φ ψ) χ) → θ)
Assertion
Ref Expression
an32s (((φ χ) ψ) → θ)

Proof of Theorem an32s
StepHypRef Expression
1 an32 496 . 2 (((φ χ) ψ) ↔ ((φ ψ) χ))
2 an32s.1 . 2 (((φ ψ) χ) → θ)
31, 2sylbi 114 1 (((φ χ) ψ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
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:  anass1rs  505  anabss1  510  fssres  5009  foco  5059  fun11iun  5090  fconstfvm  5322  isocnv  5394  f1oiso  5408  f1ocnvfv3  5444  genpassl  6507  genpassu  6508  cnegexlem3  6985  recexaplem2  7415  divap0  7445  qreccl  8351  xrlttr  8486
  Copyright terms: Public domain W3C validator