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	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
com12	|- ( ps -> ( ph -> ch ) )

Proof of Theorem com12

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2		com12.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5com 29	1 |- ( ps -> ( ph -> ch ) )

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  2847  3gencl  2848  vtocl4ga  2887  rspccv  2918  ceqex  2944  mo2icl  2996  mob  2999  euind  3004  reuind  3022  sseq2  3262  nelss  3299  difin  3458  reupick2  3507  uneqdifeqim  3595  sspw  3682  difsn  3831  ssprsseq  3856  sssnm  3858  preq12b  3874  iinss2  4044  trintssm  4224  sspwb  4332  copsexg  4360  pocl  4424  pofun  4433  sowlin  4441  reusv1  4579  alxfr  4582  ralxfrALT  4588  iunpw  4601  onsucelsucr  4630  reg2exmidlema  4656  en2lp  4676  2optocl  4827  3optocl  4828  ssrel  4838  ssrel2  4840  ssrelrel  4850  relop  4905  xpidtr  5153  trin2  5154  poltletr  5163  xp11m  5201  relcnvtr  5282  iotaval  5324  funmo  5367  fundif  5400  fss  5521  f0dom0  5561  fv3  5693  tz6.12c  5700  mpteqb  5768  funfvima  5918  f1veqaeq  5942  isoselem  5993  oprabid  6082  ovg  6193  focdmex  6308  f1o2ndf1  6424  poxp  6428  tposfn2  6497  smoel  6531  tfri3  6598  nnaass  6718  nnmordi  6749  iinerm  6841  2ecoptocl  6857  3ecoptocl  6858  th3qlem2  6872  enm  7071  xpdom2  7082  xpf1o  7097  findcard2  7146  findcard2s  7147  suppeqfsuppbi  7248  eldju2ndl  7363  updjud  7373  nninfninc  7414  distrnq0  7774  addassnq0  7777  prcdnql  7799  prcunqu  7800  nn0ge2m1nn  9560  nn0le2is012  9660  fzind  9693  nn0ind-raph  9695  zindd  9696  uzin  9887  indstr  9925  xnn0xadd0  10200  icoshft  10323  fzen  10377  uzsubsubfz  10381  elfz1b  10424  elfz0ubfz0  10459  elfz0fzfz0  10460  fz0fzelfz0  10461  elfzmlbp  10466  elfzodifsumelfzo  10546  ssfzo12bi  10570  elfzonelfzo  10575  modfzo0difsn  10757  frec2uzuzd  10764  expcllem  10912  mulexp  10940  leexp2r  10955  bernneq  11022  facdiv  11100  fundm2domnop0  11220  ccatsymb  11290  swrdnd  11351  swrdswrdlem  11396  swrdswrd  11397  pfxccatin12lem2a  11419  pfxccatin12lem1  11420  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12lem3  11424  pfxccat3  11426  swrdccat  11427  swrdccat3blem  11431  cjexp  11578  absexp  11764  clim2prod  12225  prodfap0  12231  prodfrecap  12232  prodmodc  12264  fprodabs  12302  addmodlteqALT  12545  oddge22np1  12567  nn0enne  12588  nn0o1gt2  12591  gcdneg  12678  dfgcd2  12710  rplpwr  12723  coprmdvds1  12788  qredeq  12793  cncongr1  12800  cncongr2  12801  prm2orodd  12823  nnnn0modprm0  12953  prm23lt5  12961  dvdsprmpweqnn  13034  dvdsprmpweqle  13035  oddprmdvds  13052  prmpwdvds  13053  setsn0fun  13249  isnmgm  13573  sgrpass  13621  insubm  13698  dfgrp3mlem  13811  fiinopn  14869  tgcl  14929  distop  14950  ssnei2  15022  tgcnp  15074  cnpnei  15084  cnmptcom  15163  neibl  15356  rpcxpmul2  15778  fsumdvdsmul  15859  zabsle1  15872  gausslemma2dlem1a  15931  gausslemma2dlem3  15936  lgsquad2lem2  15955  2lgs  15977  umgrnloop  16111  upgrpredgv  16141  upgredgpr  16144  wlkl1loop  16353  upgriswlkdc  16355  upgrwlkvtxedg  16359  uspgr2wlkeq  16360  wlkv0  16364  wlkres  16374  clwwlkccatlem  16395  loopclwwlkn1b  16414  umgr2cwwk2dif  16419  clwwlknonex2lem2  16433  clwwlknonex2  16434  eupth2lem3lem4fi  16468  depindlem2  16502  bj-nnbist  16516  sumdc2  16571