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

Theorem com12 30
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 29 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:  syl11  31  syl5  32  syl6com  35  mpcom  36  syli  37  pm2.27  39  pm2.43b  50  syl9r  71  com3r  77  pm2.86i  96  expcom  113  impcom  120  syl5ibcom  148  syl5ibrcom  150  pm5.501  237  impd  246  expd  249  pm3.21  255  imdistanri  428  pm2.24  561  con3rr3  573  pm2.52  592  expt  593  mtt  620  jaod  647  orel1  654  pm2.62  677  pm2.64  725  pm2.75  733  pm2.61ddc  769  peircedc  831  dcbi  855  pm5.62dc  863  pm4.83dc  869  ccased  883  3impd  1129  3expd  1132  mp3an1i  1236  pclem6  1281  simplbi2com  1349  19.21ht  1489  19.33b2  1536  equtrr  1612  spimeh  1643  cbv1  1648  equvini  1657  sbequ2  1668  ax11e  1693  ax11b  1723  sb6rf  1749  sb56  1781  exmoeudc  1979  moimv  1982  eupickbi  1998  exists2  2013  r19.12  2439  2gencl  2604  3gencl  2605  rspccv  2670  ceqex  2693  mo2icl  2742  mob  2745  euind  2750  reuind  2766  sseq2  2994  difin  3201  reupick2  3250  uneqdifeqim  3335  difsn  3528  sssnm  3552  preq12b  3568  iinss2  3736  trintssm  3897  sspwb  3979  copsexg  4008  pocl  4067  pofun  4076  sowlin  4084  reusv1  4217  alxfr  4220  ralxfrALT  4226  iunpw  4238  onsucelsucr  4261  reg2exmidlema  4286  en2lp  4305  2optocl  4444  3optocl  4445  ssrel  4455  ssrel2  4457  ssrelrel  4467  relop  4513  xpidtr  4742  trin2  4743  poltletr  4752  xp11m  4786  relcnvtr  4867  iotaval  4905  funmo  4944  fss  5081  fv3  5224  tz6.12c  5230  mpteqb  5288  funfvima  5417  f1veqaeq  5435  isoselem  5486  oprabid  5564  ovg  5666  fornex  5769  f1o2ndf1  5876  poxp  5880  tposfn2  5911  smoel  5945  tfri3  5983  nnaass  6094  nnmordi  6119  iinerm  6208  2ecoptocl  6224  3ecoptocl  6225  th3qlem2  6239  enm  6324  xpdom2  6335  findcard2  6376  findcard2s  6377  distrnq0  6614  addassnq0  6617  prcdnql  6639  prcunqu  6640  nn0ge2m1nn  8298  fzind  8411  nn0ind-raph  8413  zindd  8414  uzin  8600  indstr  8631  icoshft  8958  fzen  9008  uzsubsubfz  9012  elfz1b  9053  elfz0ubfz0  9083  elfz0fzfz0  9084  fz0fzelfz0  9085  elfzmlbmOLD  9090  elfzmlbp  9091  elfzodifsumelfzo  9158  ssfzo12bi  9182  elfzonelfzo  9187  modfzo0difsn  9339  frec2uzzd  9344  frec2uzuzd  9346  expcllem  9425  mulexp  9453  leexp2r  9468  bernneq  9530  facdiv  9599  cjexp  9714  absexp  9898  addmodlteqALT  10163  oddge22np1  10185  nn0enne  10206  nn0o1gt2  10209
  Copyright terms: Public domain W3C validator