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

Theorem com12 25
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 17 . 2 (ψψ)
2 com12.1 . 2 (φ → (ψχ))
31, 2syl5com 24 1 (ψ → (φχ))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem is referenced by:  syl5  26  syl6com  29  mpcom  30  syli  31  pm2.27  33  pm2.43b  44  syl9r  65  com3r  71  pm2.86i  90  expcom  107  impcom  114  syl5ibcom  142  syl5ibrcom  144  pm5.501  231  imp3a  240  exp3a  243  pm3.21  249  imdistanri  419  pm2.24  534  con3rr3  545  pm2.52  563  expt  564  mtt  591  jaod  617  orel1  623  pm2.62  646  pm2.64  692  pm2.75  700  pm2.61ddc  732  peircedc  789  dcbi  805  pm5.62dc  818  pm4.83dc  824  ccased  838  3impd  1071  3expd  1074  mp3an1i  1176  pclem6  1210  simplbi2com  1267  19.21ht  1410  19.33b2  1453  equtrr  1514  spimeh  1544  cbv1  1550  equvini  1559  sbequ2  1571  ax11e  1595  ax11b  1625  sb6rf  1650  sb56  1681  exmoeudc  1871  moimv  1874  eupickbi  1891  exists2  1905  r19.12  2287  2gencl  2447  3gencl  2448  rspccv  2513  ceqex  2530  mob  2580  euind  2585  reuind  2601  2eu1  2664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
  Copyright terms: Public domain W3C validator