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

Theorem com12 26
Description: Inference that swaps (commutes) antecedents in an implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com12.1 (φ → (ψχ))
Assertion
Ref Expression
com12 (ψ → (φχ))

Proof of Theorem com12
StepHypRef Expression
1 id 18 . 2 (ψψ)
2 com12.1 . 2 (φ → (ψχ))
31, 2syl5com 25 1 (ψ → (φχ))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem is referenced by:  syl5  27  syl6com  30  mpcom  31  syli  32  pm2.27  34  pm2.43b  45  syl9r  66  com3r  72  pm2.86i  91  expcom  108  impcom  115  syl5ibcom  143  syl5ibrcom  145  pm5.501  232  imp3a  241  exp3a  244  pm3.21  250  imdistanri  420  pm2.24  532  con3rr3  543  pm2.52  560  expt  561  mtt  588  jaod  613  orel1  619  pm2.62  642  pm2.64  688  pm2.75  696  jad  733  pm2.61  735  ccased  852  3impd  1086  3expd  1089  mp3an1i  1190  simplbi2com  1227  19.21t  1345  19.33b2  1376  equtrr  1419  a4ime  1446  equvini  1455  sbequ2  1466  ax11b  1514  sb6rf  1558  sb56  1591  exmoeu  1725  moimv  1731  eupickbi  1749  2eu1  1763  exists2  1773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator