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

Theorem com12 27
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 19 . 2 (ψψ)
2 com12.1 . 2 (φ → (ψχ))
31, 2syl5com 26 1 (ψ → (φχ))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  syl5  28  syl6com  31  mpcom  32  syli  33  pm2.27  35  pm2.43b  46  syl9r  67  com3r  73  pm2.86i  92  expcom  109  impcom  116  syl5ibcom  144  syl5ibrcom  146  pm5.501  233  impd  242  expd  245  pm3.21  251  imdistanri  423  pm2.24  539  con3rr3  550  pm2.52  569  expt  570  mtt  597  jaod  624  orel1  631  pm2.62  654  pm2.64  701  pm2.75  709  pm2.61ddc  746  peircedc  808  dcbi  830  pm5.62dc  838  pm4.83dc  844  ccased  858  3impd  1102  3expd  1105  mp3an1i  1208  pclem6  1248  simplbi2com  1309  19.21ht  1451  19.33b2  1498  equtrr  1574  spimeh  1605  cbv1  1610  equvini  1619  sbequ2  1630  ax11e  1655  ax11b  1685  sb6rf  1711  sb56  1743  exmoeudc  1941  moimv  1944  eupickbi  1960  exists2  1975  r19.12  2396  2gencl  2560  3gencl  2561  rspccv  2626  ceqex  2644  mo2icl  2693  mob  2696  euind  2701  reuind  2717  sseq2  2940  difin  3147  reupick2  3196  uneqdifeqim  3281  difsn  3471  sssnm  3495  preq12b  3511  iinss2  3679  trint0m  3841  sspwb  3922  copsexg  3951  pocl  4010  pofun  4019  sowlin  4027  reusv1  4136  alxfr  4139  ralxfrALT  4145  iunpw  4157  onsucelsucr  4179  en2lp  4212  2optocl  4340  3optocl  4341  ssrel  4351  ssrel2  4353  ssrelrel  4363  relop  4409  xpidtr  4638  trin2  4639  poltletr  4648  xp11m  4682  relcnvtr  4763  iotaval  4801  funmo  4839  fss  4976  fv3  5118  tz6.12c  5124  mpteqb  5182  funfvima  5311  f1veqaeq  5329  isoselem  5380  oprabid  5457  ovg  5558  fornex  5661  f1o2ndf1  5768  poxp  5771  tposfn2  5799  smoel  5833  tfri3  5871  nnaass  5975  nnmordi  5996  iinerm  6085  2ecoptocl  6101  3ecoptocl  6102  th3qlem2  6116  distrnq0  6308  addassnq0  6311  prcdnql  6332  prcunqu  6333
  Copyright terms: Public domain W3C validator