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

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2		com12.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5com 29	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl11  31  syl5  32  syl6com  35  mpcom  36  syli  37  syl2imc  39  pm2.27  40  syldc  46  pm2.43b  52  syl9r  73  com3r  79  pm2.86i  99  expcom  116  impcom  125  syl5ibcom  155  syl5ibrcom  157  pm5.501  244  impd  254  expd  258  pm3.21  264  imdistanri  446  pm2.24  626  con3rr3  638  expt  663  mtt  692  jaod  725  orel1  733  pm2.62  756  pm2.64  809  pm2.75  817  pm2.61ddc  869  peircedc  922  dcbi  945  pm5.62dc  954  pm4.83dc  960  ccased  974  3impd  1248  3expd  1251  syldbl2  1329  mp3an1i  1367  pclem6  1419  simplbi2com  1490  19.21ht  1630  19.33b2  1678  equtrr  1758  spimeh  1788  cbv1  1794  cbv1v  1796  equvini  1807  sbequ2  1818  ax11e  1845  ax11b  1875  sb6rf  1902  sb56  1935  exmoeudc  2144  moimv  2147  eupickbi  2163  exists2  2178  r19.12  2649  2gencl  2846  3gencl  2847  vtocl4ga  2886  rspccv  2917  ceqex  2943  mo2icl  2995  mob  2998  euind  3003  reuind  3021  sseq2  3261  nelss  3298  difin  3457  reupick2  3506  uneqdifeqim  3594  sspw  3681  difsn  3830  ssprsseq  3855  sssnm  3857  preq12b  3873  iinss2  4043  trintssm  4223  sspwb  4331  copsexg  4359  pocl  4423  pofun  4432  sowlin  4440  reusv1  4578  alxfr  4581  ralxfrALT  4587  iunpw  4600  onsucelsucr  4629  reg2exmidlema  4655  en2lp  4675  2optocl  4826  3optocl  4827  ssrel  4837  ssrel2  4839  ssrelrel  4849  relop  4904  xpidtr  5152  trin2  5153  poltletr  5162  xp11m  5200  relcnvtr  5281  iotaval  5323  funmo  5366  fundif  5399  fss  5520  f0dom0  5560  fv3  5692  tz6.12c  5699  mpteqb  5767  funfvima  5917  f1veqaeq  5941  isoselem  5992  oprabid  6081  ovg  6192  focdmex  6307  f1o2ndf1  6423  poxp  6427  tposfn2  6496  smoel  6530  tfri3  6597  nnaass  6717  nnmordi  6748  iinerm  6840  2ecoptocl  6856  3ecoptocl  6857  th3qlem2  6871  enm  7070  xpdom2  7081  xpf1o  7096  findcard2  7145  findcard2s  7146  suppeqfsuppbi  7247  eldju2ndl  7362  updjud  7372  nninfninc  7413  distrnq0  7770  addassnq0  7773  prcdnql  7795  prcunqu  7796  nn0ge2m1nn  9556  nn0le2is012  9656  fzind  9689  nn0ind-raph  9691  zindd  9692  uzin  9883  indstr  9921  xnn0xadd0  10196  icoshft  10319  fzen  10373  uzsubsubfz  10377  elfz1b  10420  elfz0ubfz0  10455  elfz0fzfz0  10456  fz0fzelfz0  10457  elfzmlbp  10462  elfzodifsumelfzo  10542  ssfzo12bi  10566  elfzonelfzo  10571  modfzo0difsn  10753  frec2uzuzd  10760  expcllem  10908  mulexp  10936  leexp2r  10951  bernneq  11018  facdiv  11096  fundm2domnop0  11213  ccatsymb  11283  swrdnd  11344  swrdswrdlem  11389  swrdswrd  11390  pfxccatin12lem2a  11412  pfxccatin12lem1  11413  swrdccatin2  11414  pfxccatin12lem2  11416  pfxccatin12lem3  11417  pfxccat3  11419  swrdccat  11420  swrdccat3blem  11424  cjexp  11571  absexp  11757  clim2prod  12218  prodfap0  12224  prodfrecap  12225  prodmodc  12257  fprodabs  12295  addmodlteqALT  12538  oddge22np1  12560  nn0enne  12581  nn0o1gt2  12584  gcdneg  12671  dfgcd2  12703  rplpwr  12716  coprmdvds1  12781  qredeq  12786  cncongr1  12793  cncongr2  12794  prm2orodd  12816  nnnn0modprm0  12946  prm23lt5  12954  dvdsprmpweqnn  13027  dvdsprmpweqle  13028  oddprmdvds  13045  prmpwdvds  13046  setsn0fun  13238  isnmgm  13562  sgrpass  13610  insubm  13687  dfgrp3mlem  13800  fiinopn  14856  tgcl  14916  distop  14937  ssnei2  15009  tgcnp  15061  cnpnei  15071  cnmptcom  15150  neibl  15343  rpcxpmul2  15765  fsumdvdsmul  15846  zabsle1  15859  gausslemma2dlem1a  15918  gausslemma2dlem3  15923  lgsquad2lem2  15942  2lgs  15964  umgrnloop  16098  upgrpredgv  16128  upgredgpr  16131  wlkl1loop  16340  upgriswlkdc  16342  upgrwlkvtxedg  16346  uspgr2wlkeq  16347  wlkv0  16351  wlkres  16361  clwwlkccatlem  16382  loopclwwlkn1b  16401  umgr2cwwk2dif  16406  clwwlknonex2lem2  16420  clwwlknonex2  16421  eupth2lem3lem4fi  16455  depindlem2  16489  bj-nnbist  16503  sumdc2  16558