NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  an32s GIF version

Theorem an32s 779
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 773 . 2 (((φ χ) ψ) ↔ ((φ ψ) χ))
2 an32s.1 . 2 (((φ ψ) χ) → θ)
31, 2sylbi 187 1 (((φ χ) ψ) → θ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  anass1rs  782  anabss1  787  ncfinlower  4483  nnadjoin  4520  nnpweq  4523  tfinnn  4534  fssres  5238  foco  5279  f1ores  5300  fun11iun  5305  fconstfv  5456  isocnv  5491  isomin  5496  f1oiso  5499  ncssfin  6151  nntccl  6170  tlecg  6230  ce2le  6233  nnc3n3p1  6278  nchoicelem12  6300  nchoicelem19  6307
  Copyright terms: Public domain W3C validator