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  624  con3rr3  636  expt  661  mtt  689  jaod  722  orel1  730  pm2.62  753  pm2.64  806  pm2.75  814  pm2.61ddc  866  peircedc  919  dcbi  942  pm5.62dc  951  pm4.83dc  957  ccased  971  3impd  1245  3expd  1248  syldbl2  1326  mp3an1i  1364  pclem6  1416  simplbi2com  1487  19.21ht  1627  19.33b2  1675  equtrr  1756  spimeh  1785  cbv1  1791  cbv1v  1793  equvini  1804  sbequ2  1815  ax11e  1842  ax11b  1872  sb6rf  1899  sb56  1932  exmoeudc  2141  moimv  2144  eupickbi  2160  exists2  2175  r19.12  2637  2gencl  2833  3gencl  2834  vtocl4ga  2873  rspccv  2904  ceqex  2930  mo2icl  2982  mob  2985  euind  2990  reuind  3008  sseq2  3248  nelss  3285  difin  3441  reupick2  3490  uneqdifeqim  3577  difsn  3805  ssprsseq  3830  sssnm  3832  preq12b  3848  iinss2  4018  trintssm  4198  sspwb  4302  copsexg  4330  pocl  4394  pofun  4403  sowlin  4411  reusv1  4549  alxfr  4552  ralxfrALT  4558  iunpw  4571  onsucelsucr  4600  reg2exmidlema  4626  en2lp  4646  2optocl  4796  3optocl  4797  ssrel  4807  ssrel2  4809  ssrelrel  4819  relop  4872  xpidtr  5119  trin2  5120  poltletr  5129  xp11m  5167  relcnvtr  5248  iotaval  5290  funmo  5333  fundif  5365  fss  5485  f0dom0  5519  fv3  5650  tz6.12c  5657  mpteqb  5725  funfvima  5871  f1veqaeq  5893  isoselem  5944  oprabid  6033  ovg  6144  focdmex  6260  f1o2ndf1  6374  poxp  6378  tposfn2  6412  smoel  6446  tfri3  6513  nnaass  6631  nnmordi  6662  iinerm  6754  2ecoptocl  6770  3ecoptocl  6771  th3qlem2  6785  enm  6979  xpdom2  6990  xpf1o  7005  findcard2  7051  findcard2s  7052  eldju2ndl  7239  updjud  7249  nninfninc  7290  distrnq0  7646  addassnq0  7649  prcdnql  7671  prcunqu  7672  nn0ge2m1nn  9429  nn0le2is012  9529  fzind  9562  nn0ind-raph  9564  zindd  9565  uzin  9755  indstr  9788  xnn0xadd0  10063  icoshft  10186  fzen  10239  uzsubsubfz  10243  elfz1b  10286  elfz0ubfz0  10321  elfz0fzfz0  10322  fz0fzelfz0  10323  elfzmlbp  10328  elfzodifsumelfzo  10407  ssfzo12bi  10431  elfzonelfzo  10436  modfzo0difsn  10617  frec2uzuzd  10624  expcllem  10772  mulexp  10800  leexp2r  10815  bernneq  10882  facdiv  10960  fundm2domnop0  11067  ccatsymb  11137  swrdnd  11191  swrdswrdlem  11236  swrdswrd  11237  pfxccatin12lem2a  11259  pfxccatin12lem1  11260  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12lem3  11264  pfxccat3  11266  swrdccat  11267  swrdccat3blem  11271  cjexp  11404  absexp  11590  clim2prod  12050  prodfap0  12056  prodfrecap  12057  prodmodc  12089  fprodabs  12127  addmodlteqALT  12370  oddge22np1  12392  nn0enne  12413  nn0o1gt2  12416  gcdneg  12503  dfgcd2  12535  rplpwr  12548  coprmdvds1  12613  qredeq  12618  cncongr1  12625  cncongr2  12626  prm2orodd  12648  nnnn0modprm0  12778  prm23lt5  12786  dvdsprmpweqnn  12859  dvdsprmpweqle  12860  oddprmdvds  12877  prmpwdvds  12878  setsn0fun  13069  isnmgm  13393  sgrpass  13441  insubm  13518  dfgrp3mlem  13631  fiinopn  14678  tgcl  14738  distop  14759  ssnei2  14831  tgcnp  14883  cnpnei  14893  cnmptcom  14972  neibl  15165  rpcxpmul2  15587  fsumdvdsmul  15665  zabsle1  15678  gausslemma2dlem1a  15737  gausslemma2dlem3  15742  lgsquad2lem2  15761  2lgs  15783  umgrnloop  15916  upgrpredgv  15944  upgredgpr  15947  wlkl1loop  16069  upgriswlkdc  16071  upgrwlkvtxedg  16075  uspgr2wlkeq  16076  wlkv0  16080  bj-nnbist  16108  sumdc2  16163