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  1936  exmoeudc  2146  moimv  2149  eupickbi  2165  exists2  2180  r19.12  2651  2gencl  2849  3gencl  2850  vtocl4ga  2889  rspccv  2920  ceqex  2947  mo2icl  2999  mob  3002  euind  3007  reuind  3025  sseq2  3266  nelss  3303  difin  3462  reupick2  3511  uneqdifeqim  3599  sspw  3687  difsn  3836  ssprsseq  3861  sssnm  3863  preq12b  3879  iinss2  4049  trintssm  4229  sspwb  4337  copsexg  4365  pocl  4429  pofun  4438  sowlin  4446  reusv1  4584  alxfr  4587  ralxfrALT  4593  iunpw  4606  onsucelsucr  4635  reg2exmidlema  4661  en2lp  4681  2optocl  4832  3optocl  4833  ssrel  4843  ssrel2  4845  ssrelrel  4855  relop  4910  xpidtr  5158  trin2  5159  poltletr  5168  xp11m  5206  relcnvtr  5287  iotaval  5329  funmo  5372  fundif  5405  fss  5526  f0dom0  5566  fv3  5698  tz6.12c  5705  mpteqb  5773  funfvima  5923  f1veqaeq  5948  isoselem  5999  oprabid  6090  ovg  6201  focdmex  6317  f1o2ndf1  6437  poxp  6441  tposfn2  6510  smoel  6544  tfri3  6611  nnaass  6731  nnmordi  6762  iinerm  6854  2ecoptocl  6870  3ecoptocl  6871  th3qlem2  6885  enm  7084  xpdom2  7095  xpf1o  7110  findcard2  7159  findcard2s  7160  suppeqfsuppbi  7261  eldju2ndl  7376  updjud  7386  nninfninc  7427  distrnq0  7790  addassnq0  7793  prcdnql  7815  prcunqu  7816  nn0ge2m1nn  9577  nn0le2is012  9678  fzind  9711  nn0ind-raph  9713  zindd  9714  uzin  9905  indstr  9943  xnn0xadd0  10219  icoshft  10342  fzen  10397  uzsubsubfz  10401  elfz1b  10446  elfz0ubfz0  10481  elfz0fzfz0  10482  fz0fzelfz0  10483  elfzmlbp  10488  elfzodifsumelfzo  10568  ssfzo12bi  10592  elfzonelfzo  10597  modfzo0difsn  10781  frec2uzuzd  10788  expcllem  10936  mulexp  10964  leexp2r  10979  bernneq  11047  facdiv  11125  fundm2domnop0  11245  ccatsymb  11315  swrdnd  11376  swrdswrdlem  11421  swrdswrd  11422  pfxccatin12lem2a  11444  pfxccatin12lem1  11445  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccat3  11451  swrdccat  11452  swrdccat3blem  11456  cjexp  11603  absexp  11789  clim2prod  12250  prodfap0  12256  prodfrecap  12257  prodmodc  12289  fprodabs  12327  addmodlteqALT  12570  oddge22np1  12592  nn0enne  12613  nn0o1gt2  12616  gcdneg  12703  dfgcd2  12735  rplpwr  12748  coprmdvds1  12813  qredeq  12818  cncongr1  12825  cncongr2  12826  prm2orodd  12848  nnnn0modprm0  12978  prm23lt5  12986  dvdsprmpweqnn  13059  dvdsprmpweqle  13060  oddprmdvds  13077  prmpwdvds  13078  setsn0fun  13333  isnmgm  13623  sgrpass  13671  insubm  13740  dfgrp3mlem  13853  fiinopn  14995  tgcl  15055  distop  15076  ssnei2  15148  tgcnp  15200  cnpnei  15210  cnmptcom  15289  neibl  15482  rpcxpmul2  15904  fsumdvdsmul  15985  zabsle1  15998  gausslemma2dlem1a  16057  gausslemma2dlem3  16062  lgsquad2lem2  16081  2lgs  16103  umgrnloop  16237  upgrpredgv  16267  upgredgpr  16270  wlkl1loop  16479  upgriswlkdc  16481  upgrwlkvtxedg  16485  uspgr2wlkeq  16486  wlkv0  16490  wlkres  16500  clwwlkccatlem  16521  loopclwwlkn1b  16540  umgr2cwwk2dif  16545  clwwlknonex2lem2  16559  clwwlknonex2  16560  eupth2lem3lem4fi  16594  depindlem2  16628  bj-nnbist  16642  sumdc2  16697