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  5521  fv3  5652  tz6.12c  5659  mpteqb  5727  funfvima  5875  f1veqaeq  5899  isoselem  5950  oprabid  6039  ovg  6150  focdmex  6266  f1o2ndf1  6380  poxp  6384  tposfn2  6418  smoel  6452  tfri3  6519  nnaass  6639  nnmordi  6670  iinerm  6762  2ecoptocl  6778  3ecoptocl  6779  th3qlem2  6793  enm  6987  xpdom2  6998  xpf1o  7013  findcard2  7059  findcard2s  7060  eldju2ndl  7250  updjud  7260  nninfninc  7301  distrnq0  7657  addassnq0  7660  prcdnql  7682  prcunqu  7683  nn0ge2m1nn  9440  nn0le2is012  9540  fzind  9573  nn0ind-raph  9575  zindd  9576  uzin  9767  indstr  9800  xnn0xadd0  10075  icoshft  10198  fzen  10251  uzsubsubfz  10255  elfz1b  10298  elfz0ubfz0  10333  elfz0fzfz0  10334  fz0fzelfz0  10335  elfzmlbp  10340  elfzodifsumelfzo  10419  ssfzo12bi  10443  elfzonelfzo  10448  modfzo0difsn  10629  frec2uzuzd  10636  expcllem  10784  mulexp  10812  leexp2r  10827  bernneq  10894  facdiv  10972  fundm2domnop0  11080  ccatsymb  11150  swrdnd  11206  swrdswrdlem  11251  swrdswrd  11252  pfxccatin12lem2a  11274  pfxccatin12lem1  11275  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12lem3  11279  pfxccat3  11281  swrdccat  11282  swrdccat3blem  11286  cjexp  11419  absexp  11605  clim2prod  12065  prodfap0  12071  prodfrecap  12072  prodmodc  12104  fprodabs  12142  addmodlteqALT  12385  oddge22np1  12407  nn0enne  12428  nn0o1gt2  12431  gcdneg  12518  dfgcd2  12550  rplpwr  12563  coprmdvds1  12628  qredeq  12633  cncongr1  12640  cncongr2  12641  prm2orodd  12663  nnnn0modprm0  12793  prm23lt5  12801  dvdsprmpweqnn  12874  dvdsprmpweqle  12875  oddprmdvds  12892  prmpwdvds  12893  setsn0fun  13084  isnmgm  13408  sgrpass  13456  insubm  13533  dfgrp3mlem  13646  fiinopn  14693  tgcl  14753  distop  14774  ssnei2  14846  tgcnp  14898  cnpnei  14908  cnmptcom  14987  neibl  15180  rpcxpmul2  15602  fsumdvdsmul  15680  zabsle1  15693  gausslemma2dlem1a  15752  gausslemma2dlem3  15757  lgsquad2lem2  15776  2lgs  15798  umgrnloop  15931  upgrpredgv  15959  upgredgpr  15962  wlkl1loop  16099  upgriswlkdc  16101  upgrwlkvtxedg  16105  uspgr2wlkeq  16106  wlkv0  16110  wlkres  16118  clwwlkccatlem  16137  bj-nnbist  16163  sumdc2  16218