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  622  con3rr3  634  expt  658  mtt  686  jaod  718  orel1  726  pm2.62  749  pm2.64  802  pm2.75  810  pm2.61ddc  862  peircedc  915  dcbi  938  pm5.62dc  947  pm4.83dc  953  ccased  967  3impd  1223  3expd  1226  syldbl2  1304  mp3an1i  1342  pclem6  1393  simplbi2com  1463  19.21ht  1603  19.33b2  1651  equtrr  1732  spimeh  1761  cbv1  1767  cbv1v  1769  equvini  1780  sbequ2  1791  ax11e  1818  ax11b  1848  sb6rf  1875  sb56  1908  exmoeudc  2116  moimv  2119  eupickbi  2135  exists2  2150  r19.12  2611  2gencl  2804  3gencl  2805  rspccv  2873  ceqex  2899  mo2icl  2951  mob  2954  euind  2959  reuind  2977  sseq2  3216  nelss  3253  difin  3409  reupick2  3458  uneqdifeqim  3545  difsn  3769  sssnm  3794  preq12b  3810  iinss2  3979  trintssm  4157  sspwb  4259  copsexg  4287  pocl  4349  pofun  4358  sowlin  4366  reusv1  4504  alxfr  4507  ralxfrALT  4513  iunpw  4526  onsucelsucr  4555  reg2exmidlema  4581  en2lp  4601  2optocl  4751  3optocl  4752  ssrel  4762  ssrel2  4764  ssrelrel  4774  relop  4827  xpidtr  5072  trin2  5073  poltletr  5082  xp11m  5120  relcnvtr  5201  iotaval  5242  funmo  5285  fundif  5317  fss  5436  f0dom0  5468  fv3  5598  tz6.12c  5605  mpteqb  5669  funfvima  5815  f1veqaeq  5837  isoselem  5888  oprabid  5975  ovg  6084  focdmex  6199  f1o2ndf1  6313  poxp  6317  tposfn2  6351  smoel  6385  tfri3  6452  nnaass  6570  nnmordi  6601  iinerm  6693  2ecoptocl  6709  3ecoptocl  6710  th3qlem2  6724  enm  6914  xpdom2  6925  xpf1o  6940  findcard2  6985  findcard2s  6986  eldju2ndl  7173  updjud  7183  nninfninc  7224  distrnq0  7571  addassnq0  7574  prcdnql  7596  prcunqu  7597  nn0ge2m1nn  9354  nn0le2is012  9454  fzind  9487  nn0ind-raph  9489  zindd  9490  uzin  9680  indstr  9713  xnn0xadd0  9988  icoshft  10111  fzen  10164  uzsubsubfz  10168  elfz1b  10211  elfz0ubfz0  10246  elfz0fzfz0  10247  fz0fzelfz0  10248  elfzmlbp  10253  elfzodifsumelfzo  10328  ssfzo12bi  10352  elfzonelfzo  10357  modfzo0difsn  10538  frec2uzuzd  10545  expcllem  10693  mulexp  10721  leexp2r  10736  bernneq  10803  facdiv  10881  fundm2domnop0  10988  ccatsymb  11056  cjexp  11175  absexp  11361  clim2prod  11821  prodfap0  11827  prodfrecap  11828  prodmodc  11860  fprodabs  11898  addmodlteqALT  12141  oddge22np1  12163  nn0enne  12184  nn0o1gt2  12187  gcdneg  12274  dfgcd2  12306  rplpwr  12319  coprmdvds1  12384  qredeq  12389  cncongr1  12396  cncongr2  12397  prm2orodd  12419  nnnn0modprm0  12549  prm23lt5  12557  dvdsprmpweqnn  12630  dvdsprmpweqle  12631  oddprmdvds  12648  prmpwdvds  12649  setsn0fun  12840  isnmgm  13163  sgrpass  13211  insubm  13288  dfgrp3mlem  13401  fiinopn  14447  tgcl  14507  distop  14528  ssnei2  14600  tgcnp  14652  cnpnei  14662  cnmptcom  14741  neibl  14934  rpcxpmul2  15356  fsumdvdsmul  15434  zabsle1  15447  gausslemma2dlem1a  15506  gausslemma2dlem3  15511  lgsquad2lem2  15530  2lgs  15552  bj-nnbist  15642  sumdc2  15697