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  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  5885  f1veqaeq  5909  isoselem  5960  oprabid  6049  ovg  6160  focdmex  6276  f1o2ndf1  6392  poxp  6396  tposfn2  6431  smoel  6465  tfri3  6532  nnaass  6652  nnmordi  6683  iinerm  6775  2ecoptocl  6791  3ecoptocl  6792  th3qlem2  6806  enm  7003  xpdom2  7014  xpf1o  7029  findcard2  7077  findcard2s  7078  eldju2ndl  7270  updjud  7280  nninfninc  7321  distrnq0  7678  addassnq0  7681  prcdnql  7703  prcunqu  7704  nn0ge2m1nn  9461  nn0le2is012  9561  fzind  9594  nn0ind-raph  9596  zindd  9597  uzin  9788  indstr  9826  xnn0xadd0  10101  icoshft  10224  fzen  10277  uzsubsubfz  10281  elfz1b  10324  elfz0ubfz0  10359  elfz0fzfz0  10360  fz0fzelfz0  10361  elfzmlbp  10366  elfzodifsumelfzo  10445  ssfzo12bi  10469  elfzonelfzo  10474  modfzo0difsn  10656  frec2uzuzd  10663  expcllem  10811  mulexp  10839  leexp2r  10854  bernneq  10921  facdiv  10999  fundm2domnop0  11108  ccatsymb  11178  swrdnd  11239  swrdswrdlem  11284  swrdswrd  11285  pfxccatin12lem2a  11307  pfxccatin12lem1  11308  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccat3  11314  swrdccat  11315  swrdccat3blem  11319  cjexp  11453  absexp  11639  clim2prod  12099  prodfap0  12105  prodfrecap  12106  prodmodc  12138  fprodabs  12176  addmodlteqALT  12419  oddge22np1  12441  nn0enne  12462  nn0o1gt2  12465  gcdneg  12552  dfgcd2  12584  rplpwr  12597  coprmdvds1  12662  qredeq  12667  cncongr1  12674  cncongr2  12675  prm2orodd  12697  nnnn0modprm0  12827  prm23lt5  12835  dvdsprmpweqnn  12908  dvdsprmpweqle  12909  oddprmdvds  12926  prmpwdvds  12927  setsn0fun  13118  isnmgm  13442  sgrpass  13490  insubm  13567  dfgrp3mlem  13680  fiinopn  14727  tgcl  14787  distop  14808  ssnei2  14880  tgcnp  14932  cnpnei  14942  cnmptcom  15021  neibl  15214  rpcxpmul2  15636  fsumdvdsmul  15714  zabsle1  15727  gausslemma2dlem1a  15786  gausslemma2dlem3  15791  lgsquad2lem2  15810  2lgs  15832  umgrnloop  15966  upgrpredgv  15996  upgredgpr  15999  wlkl1loop  16208  upgriswlkdc  16210  upgrwlkvtxedg  16214  uspgr2wlkeq  16215  wlkv0  16219  wlkres  16229  clwwlkccatlem  16250  loopclwwlkn1b  16269  umgr2cwwk2dif  16274  clwwlknonex2lem2  16288  clwwlknonex2  16289  bj-nnbist  16340  sumdc2  16395