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  691  jaod  724  orel1  732  pm2.62  755  pm2.64  808  pm2.75  816  pm2.61ddc  868  peircedc  921  dcbi  944  pm5.62dc  953  pm4.83dc  959  ccased  973  3impd  1247  3expd  1250  syldbl2  1328  mp3an1i  1366  pclem6  1418  simplbi2com  1489  19.21ht  1629  19.33b2  1677  equtrr  1758  spimeh  1787  cbv1  1793  cbv1v  1795  equvini  1806  sbequ2  1817  ax11e  1844  ax11b  1874  sb6rf  1901  sb56  1934  exmoeudc  2143  moimv  2146  eupickbi  2162  exists2  2177  r19.12  2639  2gencl  2836  3gencl  2837  vtocl4ga  2876  rspccv  2907  ceqex  2933  mo2icl  2985  mob  2988  euind  2993  reuind  3011  sseq2  3251  nelss  3288  difin  3444  reupick2  3493  uneqdifeqim  3580  difsn  3810  ssprsseq  3835  sssnm  3837  preq12b  3853  iinss2  4023  trintssm  4203  sspwb  4308  copsexg  4336  pocl  4400  pofun  4409  sowlin  4417  reusv1  4555  alxfr  4558  ralxfrALT  4564  iunpw  4577  onsucelsucr  4606  reg2exmidlema  4632  en2lp  4652  2optocl  4803  3optocl  4804  ssrel  4814  ssrel2  4816  ssrelrel  4826  relop  4880  xpidtr  5127  trin2  5128  poltletr  5137  xp11m  5175  relcnvtr  5256  iotaval  5298  funmo  5341  fundif  5374  fss  5494  f0dom0  5530  fv3  5662  tz6.12c  5669  mpteqb  5737  funfvima  5886  f1veqaeq  5910  isoselem  5961  oprabid  6050  ovg  6161  focdmex  6277  f1o2ndf1  6393  poxp  6397  tposfn2  6432  smoel  6466  tfri3  6533  nnaass  6653  nnmordi  6684  iinerm  6776  2ecoptocl  6792  3ecoptocl  6793  th3qlem2  6807  enm  7004  xpdom2  7015  xpf1o  7030  findcard2  7078  findcard2s  7079  eldju2ndl  7271  updjud  7281  nninfninc  7322  distrnq0  7679  addassnq0  7682  prcdnql  7704  prcunqu  7705  nn0ge2m1nn  9462  nn0le2is012  9562  fzind  9595  nn0ind-raph  9597  zindd  9598  uzin  9789  indstr  9827  xnn0xadd0  10102  icoshft  10225  fzen  10278  uzsubsubfz  10282  elfz1b  10325  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  elfzmlbp  10367  elfzodifsumelfzo  10447  ssfzo12bi  10471  elfzonelfzo  10476  modfzo0difsn  10658  frec2uzuzd  10665  expcllem  10813  mulexp  10841  leexp2r  10856  bernneq  10923  facdiv  11001  fundm2domnop0  11110  ccatsymb  11180  swrdnd  11241  swrdswrdlem  11286  swrdswrd  11287  pfxccatin12lem2a  11309  pfxccatin12lem1  11310  swrdccatin2  11311  pfxccatin12lem2  11313  pfxccatin12lem3  11314  pfxccat3  11316  swrdccat  11317  swrdccat3blem  11321  cjexp  11455  absexp  11641  clim2prod  12102  prodfap0  12108  prodfrecap  12109  prodmodc  12141  fprodabs  12179  addmodlteqALT  12422  oddge22np1  12444  nn0enne  12465  nn0o1gt2  12468  gcdneg  12555  dfgcd2  12587  rplpwr  12600  coprmdvds1  12665  qredeq  12670  cncongr1  12677  cncongr2  12678  prm2orodd  12700  nnnn0modprm0  12830  prm23lt5  12838  dvdsprmpweqnn  12911  dvdsprmpweqle  12912  oddprmdvds  12929  prmpwdvds  12930  setsn0fun  13121  isnmgm  13445  sgrpass  13493  insubm  13570  dfgrp3mlem  13683  fiinopn  14731  tgcl  14791  distop  14812  ssnei2  14884  tgcnp  14936  cnpnei  14946  cnmptcom  15025  neibl  15218  rpcxpmul2  15640  fsumdvdsmul  15718  zabsle1  15731  gausslemma2dlem1a  15790  gausslemma2dlem3  15795  lgsquad2lem2  15814  2lgs  15836  umgrnloop  15970  upgrpredgv  16000  upgredgpr  16003  wlkl1loop  16212  upgriswlkdc  16214  upgrwlkvtxedg  16218  uspgr2wlkeq  16219  wlkv0  16223  wlkres  16233  clwwlkccatlem  16254  loopclwwlkn1b  16273  umgr2cwwk2dif  16278  clwwlknonex2lem2  16292  clwwlknonex2  16293  eupth2lem3lem4fi  16327  depindlem2  16347  bj-nnbist  16361  sumdc2  16416