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  659  mtt  687  jaod  719  orel1  727  pm2.62  750  pm2.64  803  pm2.75  811  pm2.61ddc  863  peircedc  916  dcbi  939  pm5.62dc  948  pm4.83dc  954  ccased  968  3impd  1224  3expd  1227  syldbl2  1305  mp3an1i  1343  pclem6  1394  simplbi2com  1464  19.21ht  1604  19.33b2  1652  equtrr  1733  spimeh  1762  cbv1  1768  cbv1v  1770  equvini  1781  sbequ2  1792  ax11e  1819  ax11b  1849  sb6rf  1876  sb56  1909  exmoeudc  2117  moimv  2120  eupickbi  2136  exists2  2151  r19.12  2612  2gencl  2805  3gencl  2806  rspccv  2874  ceqex  2900  mo2icl  2952  mob  2955  euind  2960  reuind  2978  sseq2  3217  nelss  3254  difin  3410  reupick2  3459  uneqdifeqim  3546  difsn  3770  sssnm  3795  preq12b  3811  iinss2  3980  trintssm  4158  sspwb  4260  copsexg  4288  pocl  4350  pofun  4359  sowlin  4367  reusv1  4505  alxfr  4508  ralxfrALT  4514  iunpw  4527  onsucelsucr  4556  reg2exmidlema  4582  en2lp  4602  2optocl  4752  3optocl  4753  ssrel  4763  ssrel2  4765  ssrelrel  4775  relop  4828  xpidtr  5073  trin2  5074  poltletr  5083  xp11m  5121  relcnvtr  5202  iotaval  5243  funmo  5286  fundif  5318  fss  5437  f0dom0  5469  fv3  5599  tz6.12c  5606  mpteqb  5670  funfvima  5816  f1veqaeq  5838  isoselem  5889  oprabid  5976  ovg  6085  focdmex  6200  f1o2ndf1  6314  poxp  6318  tposfn2  6352  smoel  6386  tfri3  6453  nnaass  6571  nnmordi  6602  iinerm  6694  2ecoptocl  6710  3ecoptocl  6711  th3qlem2  6725  enm  6915  xpdom2  6926  xpf1o  6941  findcard2  6986  findcard2s  6987  eldju2ndl  7174  updjud  7184  nninfninc  7225  distrnq0  7572  addassnq0  7575  prcdnql  7597  prcunqu  7598  nn0ge2m1nn  9355  nn0le2is012  9455  fzind  9488  nn0ind-raph  9490  zindd  9491  uzin  9681  indstr  9714  xnn0xadd0  9989  icoshft  10112  fzen  10165  uzsubsubfz  10169  elfz1b  10212  elfz0ubfz0  10247  elfz0fzfz0  10248  fz0fzelfz0  10249  elfzmlbp  10254  elfzodifsumelfzo  10330  ssfzo12bi  10354  elfzonelfzo  10359  modfzo0difsn  10540  frec2uzuzd  10547  expcllem  10695  mulexp  10723  leexp2r  10738  bernneq  10805  facdiv  10883  fundm2domnop0  10990  ccatsymb  11058  swrdnd  11112  cjexp  11204  absexp  11390  clim2prod  11850  prodfap0  11856  prodfrecap  11857  prodmodc  11889  fprodabs  11927  addmodlteqALT  12170  oddge22np1  12192  nn0enne  12213  nn0o1gt2  12216  gcdneg  12303  dfgcd2  12335  rplpwr  12348  coprmdvds1  12413  qredeq  12418  cncongr1  12425  cncongr2  12426  prm2orodd  12448  nnnn0modprm0  12578  prm23lt5  12586  dvdsprmpweqnn  12659  dvdsprmpweqle  12660  oddprmdvds  12677  prmpwdvds  12678  setsn0fun  12869  isnmgm  13192  sgrpass  13240  insubm  13317  dfgrp3mlem  13430  fiinopn  14476  tgcl  14536  distop  14557  ssnei2  14629  tgcnp  14681  cnpnei  14691  cnmptcom  14770  neibl  14963  rpcxpmul2  15385  fsumdvdsmul  15463  zabsle1  15476  gausslemma2dlem1a  15535  gausslemma2dlem3  15540  lgsquad2lem2  15559  2lgs  15581  bj-nnbist  15680  sumdc2  15735