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

Theorem com23 72
Description: Commutation of antecedents. Swap 2nd and 3rd. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com3.1 (φ → (ψ → (χθ)))
Assertion
Ref Expression
com23 (φ → (χ → (ψθ)))

Proof of Theorem com23
StepHypRef Expression
1 com3.1 . 2 (φ → (ψ → (χθ)))
2 pm2.27 35 . 2 (χ → ((χθ) → θ))
31, 2syl9 66 1 (φ → (χ → (ψθ)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com3r  73  com13  74  pm2.04  76  pm2.86d  93  impancom  427  dedlem0b  919  3com23  1157  exp3acom23  1372  ax12b  1689  a16g  1945  cbv1h  1978  sbied  2036  sbequi  2059  ax11indn  2195  eqrdav  2352  ralrimdva  2704  ralrimdvva  2709  ceqsalt  2881  vtoclgft  2905  reu6  3025  sbciegft  3076  reuss2  3535  reupick  3539  nnsucelr  4428  nndisjeq  4429  ltfintri  4466  ssfin  4470  evenodddisj  4516  nnadjoin  4520  sfintfin  4532  tfinnn  4534  spfinsfincl  4539  funssres  5144  funcnvuni  5161  fv3  5341  tz6.12-1  5344  funfvima2  5460  isoini  5497  f1o2d  5727  fnpprod  5843  enpw1  6062  enprmaplem3  6078  nclenn  6249  nchoicelem6  6294  nchoicelem12  6300  nchoicelem17  6305
  Copyright terms: Public domain W3C validator