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  1936  exmoeudc  2146  moimv  2149  eupickbi  2165  exists2  2180  r19.12  2651  2gencl  2849  3gencl  2850  vtocl4ga  2889  rspccv  2920  ceqex  2946  mo2icl  2998  mob  3001  euind  3006  reuind  3024  sseq2  3264  nelss  3301  difin  3460  reupick2  3509  uneqdifeqim  3597  sspw  3684  difsn  3833  ssprsseq  3858  sssnm  3860  preq12b  3876  iinss2  4046  trintssm  4226  sspwb  4334  copsexg  4362  pocl  4426  pofun  4435  sowlin  4443  reusv1  4581  alxfr  4584  ralxfrALT  4590  iunpw  4603  onsucelsucr  4632  reg2exmidlema  4658  en2lp  4678  2optocl  4829  3optocl  4830  ssrel  4840  ssrel2  4842  ssrelrel  4852  relop  4907  xpidtr  5155  trin2  5156  poltletr  5165  xp11m  5203  relcnvtr  5284  iotaval  5326  funmo  5369  fundif  5402  fss  5523  f0dom0  5563  fv3  5695  tz6.12c  5702  mpteqb  5770  funfvima  5920  f1veqaeq  5944  isoselem  5995  oprabid  6084  ovg  6195  focdmex  6310  f1o2ndf1  6426  poxp  6430  tposfn2  6499  smoel  6533  tfri3  6600  nnaass  6720  nnmordi  6751  iinerm  6843  2ecoptocl  6859  3ecoptocl  6860  th3qlem2  6874  enm  7073  xpdom2  7084  xpf1o  7099  findcard2  7148  findcard2s  7149  suppeqfsuppbi  7250  eldju2ndl  7365  updjud  7375  nninfninc  7416  distrnq0  7779  addassnq0  7782  prcdnql  7804  prcunqu  7805  nn0ge2m1nn  9565  nn0le2is012  9666  fzind  9699  nn0ind-raph  9701  zindd  9702  uzin  9893  indstr  9931  xnn0xadd0  10206  icoshft  10329  fzen  10383  uzsubsubfz  10387  elfz1b  10431  elfz0ubfz0  10466  elfz0fzfz0  10467  fz0fzelfz0  10468  elfzmlbp  10473  elfzodifsumelfzo  10553  ssfzo12bi  10577  elfzonelfzo  10582  modfzo0difsn  10764  frec2uzuzd  10771  expcllem  10919  mulexp  10947  leexp2r  10962  bernneq  11030  facdiv  11108  fundm2domnop0  11228  ccatsymb  11298  swrdnd  11359  swrdswrdlem  11404  swrdswrd  11405  pfxccatin12lem2a  11427  pfxccatin12lem1  11428  swrdccatin2  11429  pfxccatin12lem2  11431  pfxccatin12lem3  11432  pfxccat3  11434  swrdccat  11435  swrdccat3blem  11439  cjexp  11586  absexp  11772  clim2prod  12233  prodfap0  12239  prodfrecap  12240  prodmodc  12272  fprodabs  12310  addmodlteqALT  12553  oddge22np1  12575  nn0enne  12596  nn0o1gt2  12599  gcdneg  12686  dfgcd2  12718  rplpwr  12731  coprmdvds1  12796  qredeq  12801  cncongr1  12808  cncongr2  12809  prm2orodd  12831  nnnn0modprm0  12961  prm23lt5  12969  dvdsprmpweqnn  13042  dvdsprmpweqle  13043  oddprmdvds  13060  prmpwdvds  13061  setsn0fun  13270  isnmgm  13594  sgrpass  13642  insubm  13719  dfgrp3mlem  13832  fiinopn  14918  tgcl  14978  distop  14999  ssnei2  15071  tgcnp  15123  cnpnei  15133  cnmptcom  15212  neibl  15405  rpcxpmul2  15827  fsumdvdsmul  15908  zabsle1  15921  gausslemma2dlem1a  15980  gausslemma2dlem3  15985  lgsquad2lem2  16004  2lgs  16026  umgrnloop  16160  upgrpredgv  16190  upgredgpr  16193  wlkl1loop  16402  upgriswlkdc  16404  upgrwlkvtxedg  16408  uspgr2wlkeq  16409  wlkv0  16413  wlkres  16423  clwwlkccatlem  16444  loopclwwlkn1b  16463  umgr2cwwk2dif  16468  clwwlknonex2lem2  16482  clwwlknonex2  16483  eupth2lem3lem4fi  16517  depindlem2  16551  bj-nnbist  16565  sumdc2  16620