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. (The proof was 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  421  pm2.24  533  con3rr3  544  pm2.52  561  expt  562  mtt  589  jaod  614  orel1  620  pm2.62  643  pm2.64  689  pm2.75  697  jad  739  pm2.61  742  ccased  882  dedlem0b  888  3impd  1130  3expd  1133  mp3an1i  1234  meredith  1250  simplbi2com  1331  a9wa9lem2  1405  a9wa9lem2OLD  1406  a9wa9lem6OLD  1411  19.21t  1477  19.33b2  1519  equtrr  1568  a4ime  1593  equvini  1602  sbequ2  1613  ax11b  1656  sb6rf  1698  sb56  1704  exmoeu  1866  moimv  1872  eupickbi  1890  2eu1  1904  exists2  1914
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator