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  624  con3rr3  636  expt  661  mtt  689  jaod  721  orel1  729  pm2.62  752  pm2.64  805  pm2.75  813  pm2.61ddc  865  peircedc  918  dcbi  941  pm5.62dc  950  pm4.83dc  956  ccased  970  3impd  1226  3expd  1229  syldbl2  1307  mp3an1i  1345  pclem6  1396  simplbi2com  1467  19.21ht  1607  19.33b2  1655  equtrr  1736  spimeh  1765  cbv1  1771  cbv1v  1773  equvini  1784  sbequ2  1795  ax11e  1822  ax11b  1852  sb6rf  1879  sb56  1912  exmoeudc  2121  moimv  2124  eupickbi  2140  exists2  2155  r19.12  2617  2gencl  2813  3gencl  2814  vtocl4ga  2853  rspccv  2884  ceqex  2910  mo2icl  2962  mob  2965  euind  2970  reuind  2988  sseq2  3228  nelss  3265  difin  3421  reupick2  3470  uneqdifeqim  3557  difsn  3784  ssprsseq  3809  sssnm  3811  preq12b  3827  iinss2  3997  trintssm  4177  sspwb  4281  copsexg  4309  pocl  4371  pofun  4380  sowlin  4388  reusv1  4526  alxfr  4529  ralxfrALT  4535  iunpw  4548  onsucelsucr  4577  reg2exmidlema  4603  en2lp  4623  2optocl  4773  3optocl  4774  ssrel  4784  ssrel2  4786  ssrelrel  4796  relop  4849  xpidtr  5095  trin2  5096  poltletr  5105  xp11m  5143  relcnvtr  5224  iotaval  5266  funmo  5309  fundif  5341  fss  5461  f0dom0  5495  fv3  5626  tz6.12c  5633  mpteqb  5698  funfvima  5844  f1veqaeq  5866  isoselem  5917  oprabid  6006  ovg  6115  focdmex  6230  f1o2ndf1  6344  poxp  6348  tposfn2  6382  smoel  6416  tfri3  6483  nnaass  6601  nnmordi  6632  iinerm  6724  2ecoptocl  6740  3ecoptocl  6741  th3qlem2  6755  enm  6947  xpdom2  6958  xpf1o  6973  findcard2  7019  findcard2s  7020  eldju2ndl  7207  updjud  7217  nninfninc  7258  distrnq0  7614  addassnq0  7617  prcdnql  7639  prcunqu  7640  nn0ge2m1nn  9397  nn0le2is012  9497  fzind  9530  nn0ind-raph  9532  zindd  9533  uzin  9723  indstr  9756  xnn0xadd0  10031  icoshft  10154  fzen  10207  uzsubsubfz  10211  elfz1b  10254  elfz0ubfz0  10289  elfz0fzfz0  10290  fz0fzelfz0  10291  elfzmlbp  10296  elfzodifsumelfzo  10374  ssfzo12bi  10398  elfzonelfzo  10403  modfzo0difsn  10584  frec2uzuzd  10591  expcllem  10739  mulexp  10767  leexp2r  10782  bernneq  10849  facdiv  10927  fundm2domnop0  11034  ccatsymb  11103  swrdnd  11157  swrdswrdlem  11202  swrdswrd  11203  pfxccatin12lem2a  11225  pfxccatin12lem1  11226  swrdccatin2  11227  pfxccatin12lem2  11229  pfxccatin12lem3  11230  pfxccat3  11232  swrdccat  11233  swrdccat3blem  11237  cjexp  11370  absexp  11556  clim2prod  12016  prodfap0  12022  prodfrecap  12023  prodmodc  12055  fprodabs  12093  addmodlteqALT  12336  oddge22np1  12358  nn0enne  12379  nn0o1gt2  12382  gcdneg  12469  dfgcd2  12501  rplpwr  12514  coprmdvds1  12579  qredeq  12584  cncongr1  12591  cncongr2  12592  prm2orodd  12614  nnnn0modprm0  12744  prm23lt5  12752  dvdsprmpweqnn  12825  dvdsprmpweqle  12826  oddprmdvds  12843  prmpwdvds  12844  setsn0fun  13035  isnmgm  13359  sgrpass  13407  insubm  13484  dfgrp3mlem  13597  fiinopn  14643  tgcl  14703  distop  14724  ssnei2  14796  tgcnp  14848  cnpnei  14858  cnmptcom  14937  neibl  15130  rpcxpmul2  15552  fsumdvdsmul  15630  zabsle1  15643  gausslemma2dlem1a  15702  gausslemma2dlem3  15707  lgsquad2lem2  15726  2lgs  15748  umgrnloop  15881  upgrpredgv  15909  upgredgpr  15912  bj-nnbist  16018  sumdc2  16073