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  450  pm2.24  630  con3rr3  642  expt  667  mtt  696  jaod  729  orel1  737  pm2.62  760  pm2.64  813  pm2.75  821  pm2.61ddc  873  peircedc  926  dcbi  949  pm5.62dc  958  pm4.83dc  964  ccased  978  3impd  1252  3expd  1255  syldbl2  1333  mp3an1i  1371  pclem6  1423  simplbi2com  1494  19.21ht  1634  19.33b2  1682  equtrr  1762  spimeh  1792  cbv1  1798  cbv1v  1800  equvini  1811  sbequ2  1822  ax11e  1849  ax11b  1879  sb6rf  1906  sb56  1940  exmoeudc  2150  moimv  2153  eupickbi  2169  exists2  2184  r19.12  2657  2gencl  2855  3gencl  2856  vtocl4ga  2895  rspccv  2926  ceqex  2953  mo2icl  3005  mob  3008  euind  3013  reuind  3031  sseq2  3272  nelss  3309  difin  3468  reupick2  3519  uneqdifeqim  3610  sspw  3698  difsn  3847  ssprsseq  3872  sssnm  3874  preq12b  3890  iinss2  4060  trintssm  4240  sspwb  4351  copsexg  4379  pocl  4443  pofun  4452  sowlin  4460  reusv1  4599  alxfr  4602  ralxfrALT  4608  iunpw  4621  onsucelsucr  4650  reg2exmidlema  4676  en2lp  4696  2optocl  4847  3optocl  4848  ssrel  4858  ssrel2  4860  ssrelrel  4870  relop  4925  xpidtr  5173  trin2  5174  poltletr  5183  xp11m  5221  relcnvtr  5302  iotaval  5344  funmo  5387  fundif  5420  fss  5541  f0dom0  5581  fv3  5713  tz6.12c  5720  mpteqb  5790  funfvima  5940  f1veqaeq  5965  isoselem  6016  oprabid  6107  ovg  6218  focdmex  6334  f1o2ndf1  6454  poxp  6458  tposfn2  6527  smoel  6561  tfri3  6628  nnaass  6748  nnmordi  6779  iinerm  6871  2ecoptocl  6887  3ecoptocl  6888  th3qlem2  6902  enm  7108  xpdom2  7119  xpf1o  7134  findcard2  7183  findcard2s  7184  suppeqfsuppbi  7285  eldju2ndl  7402  updjud  7412  nninfninc  7453  distrnq0  7816  addassnq0  7819  prcdnql  7841  prcunqu  7842  nn0ge2m1nn  9606  nn0le2is012  9707  fzind  9740  nn0ind-raph  9742  zindd  9743  uzin  9934  indstr  9972  xnn0xadd0  10248  icoshft  10371  fzen  10426  uzsubsubfz  10430  elfz1b  10475  elfz0ubfz0  10510  elfz0fzfz0  10511  fz0fzelfz0  10512  elfzmlbp  10517  elfzodifsumelfzo  10597  ssfzo12bi  10621  elfzonelfzo  10626  modfzo0difsn  10810  frec2uzuzd  10817  expcllem  10965  mulexp  10993  leexp2r  11008  bernneq  11076  facdiv  11154  fundm2domnop0  11278  ccatsymb  11348  swrdnd  11409  swrdswrdlem  11454  swrdswrd  11455  pfxccatin12lem2a  11477  pfxccatin12lem1  11478  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12lem3  11482  pfxccat3  11484  swrdccat  11485  swrdccat3blem  11489  cjexp  11636  absexp  11823  clim2prod  12284  prodfap0  12290  prodfrecap  12291  prodmodc  12323  fprodabs  12361  addmodlteqALT  12604  oddge22np1  12626  nn0enne  12647  nn0o1gt2  12650  gcdneg  12737  dfgcd2  12769  rplpwr  12782  coprmdvds1  12847  qredeq  12852  cncongr1  12859  cncongr2  12860  prm2orodd  12882  nnnn0modprm0  13012  prm23lt5  13020  dvdsprmpweqnn  13093  dvdsprmpweqle  13094  oddprmdvds  13111  prmpwdvds  13112  setsn0fun  13367  isnmgm  13657  sgrpass  13700  insubm  13769  dfgrp3mlem  13880  fiinopn  15028  tgcl  15088  distop  15109  ssnei2  15181  tgcnp  15233  cnpnei  15243  cnmptcom  15322  neibl  15515  rpcxpmul2  15938  fsumdvdsmul  16019  zabsle1  16032  gausslemma2dlem1a  16091  gausslemma2dlem3  16096  lgsquad2lem2  16115  2lgs  16137  umgrnloop  16271  upgrpredgv  16301  upgredgpr  16304  wlkl1loop  16513  upgriswlkdc  16515  upgrwlkvtxedg  16519  uspgr2wlkeq  16520  wlkv0  16524  wlkres  16534  clwwlkccatlem  16555  loopclwwlkn1b  16574  umgr2cwwk2dif  16579  clwwlknonex2lem2  16593  clwwlknonex2  16594  eupth2lem3lem4fi  16628  depindlem2  16662  bj-nnbist  16686  sumdc2  16741