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  3804  ssprsseq  3829  sssnm  3831  preq12b  3847  iinss2  4017  trintssm  4197  sspwb  4301  copsexg  4329  pocl  4393  pofun  4402  sowlin  4410  reusv1  4548  alxfr  4551  ralxfrALT  4557  iunpw  4570  onsucelsucr  4599  reg2exmidlema  4625  en2lp  4645  2optocl  4795  3optocl  4796  ssrel  4806  ssrel2  4808  ssrelrel  4818  relop  4871  xpidtr  5118  trin2  5119  poltletr  5128  xp11m  5166  relcnvtr  5247  iotaval  5289  funmo  5332  fundif  5364  fss  5484  f0dom0  5518  fv3  5649  tz6.12c  5656  mpteqb  5724  funfvima  5870  f1veqaeq  5892  isoselem  5943  oprabid  6032  ovg  6143  focdmex  6258  f1o2ndf1  6372  poxp  6376  tposfn2  6410  smoel  6444  tfri3  6511  nnaass  6629  nnmordi  6660  iinerm  6752  2ecoptocl  6768  3ecoptocl  6769  th3qlem2  6783  enm  6975  xpdom2  6986  xpf1o  7001  findcard2  7047  findcard2s  7048  eldju2ndl  7235  updjud  7245  nninfninc  7286  distrnq0  7642  addassnq0  7645  prcdnql  7667  prcunqu  7668  nn0ge2m1nn  9425  nn0le2is012  9525  fzind  9558  nn0ind-raph  9560  zindd  9561  uzin  9751  indstr  9784  xnn0xadd0  10059  icoshft  10182  fzen  10235  uzsubsubfz  10239  elfz1b  10282  elfz0ubfz0  10317  elfz0fzfz0  10318  fz0fzelfz0  10319  elfzmlbp  10324  elfzodifsumelfzo  10402  ssfzo12bi  10426  elfzonelfzo  10431  modfzo0difsn  10612  frec2uzuzd  10619  expcllem  10767  mulexp  10795  leexp2r  10810  bernneq  10877  facdiv  10955  fundm2domnop0  11062  ccatsymb  11132  swrdnd  11186  swrdswrdlem  11231  swrdswrd  11232  pfxccatin12lem2a  11254  pfxccatin12lem1  11255  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12lem3  11259  pfxccat3  11261  swrdccat  11262  swrdccat3blem  11266  cjexp  11399  absexp  11585  clim2prod  12045  prodfap0  12051  prodfrecap  12052  prodmodc  12084  fprodabs  12122  addmodlteqALT  12365  oddge22np1  12387  nn0enne  12408  nn0o1gt2  12411  gcdneg  12498  dfgcd2  12530  rplpwr  12543  coprmdvds1  12608  qredeq  12613  cncongr1  12620  cncongr2  12621  prm2orodd  12643  nnnn0modprm0  12773  prm23lt5  12781  dvdsprmpweqnn  12854  dvdsprmpweqle  12855  oddprmdvds  12872  prmpwdvds  12873  setsn0fun  13064  isnmgm  13388  sgrpass  13436  insubm  13513  dfgrp3mlem  13626  fiinopn  14672  tgcl  14732  distop  14753  ssnei2  14825  tgcnp  14877  cnpnei  14887  cnmptcom  14966  neibl  15159  rpcxpmul2  15581  fsumdvdsmul  15659  zabsle1  15672  gausslemma2dlem1a  15731  gausslemma2dlem3  15736  lgsquad2lem2  15755  2lgs  15777  umgrnloop  15910  upgrpredgv  15938  upgredgpr  15941  bj-nnbist  16066  sumdc2  16121