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  621  con3rr3  633  expt  657  mtt  685  jaod  717  orel1  725  pm2.62  748  pm2.64  801  pm2.75  809  pm2.61ddc  861  peircedc  914  dcbi  936  pm5.62dc  945  pm4.83dc  951  ccased  965  3impd  1221  3expd  1224  mp3an1i  1330  pclem6  1374  simplbi2com  1444  19.21ht  1581  19.33b2  1629  equtrr  1710  spimeh  1739  cbv1  1745  cbv1v  1747  equvini  1758  sbequ2  1769  ax11e  1796  ax11b  1826  sb6rf  1853  sb56  1885  exmoeudc  2089  moimv  2092  eupickbi  2108  exists2  2123  r19.12  2583  2gencl  2772  3gencl  2773  rspccv  2840  ceqex  2866  mo2icl  2918  mob  2921  euind  2926  reuind  2944  sseq2  3181  nelss  3218  difin  3374  reupick2  3423  uneqdifeqim  3510  difsn  3731  sssnm  3756  preq12b  3772  iinss2  3941  trintssm  4119  sspwb  4218  copsexg  4246  pocl  4305  pofun  4314  sowlin  4322  reusv1  4460  alxfr  4463  ralxfrALT  4469  iunpw  4482  onsucelsucr  4509  reg2exmidlema  4535  en2lp  4555  2optocl  4705  3optocl  4706  ssrel  4716  ssrel2  4718  ssrelrel  4728  relop  4779  xpidtr  5021  trin2  5022  poltletr  5031  xp11m  5069  relcnvtr  5150  iotaval  5191  funmo  5233  fss  5379  f0dom0  5411  fv3  5540  tz6.12c  5547  mpteqb  5609  funfvima  5751  f1veqaeq  5773  isoselem  5824  oprabid  5910  ovg  6016  focdmex  6119  f1o2ndf1  6232  poxp  6236  tposfn2  6270  smoel  6304  tfri3  6371  nnaass  6489  nnmordi  6520  iinerm  6610  2ecoptocl  6626  3ecoptocl  6627  th3qlem2  6641  enm  6823  xpdom2  6834  xpf1o  6847  findcard2  6892  findcard2s  6893  eldju2ndl  7074  updjud  7084  distrnq0  7461  addassnq0  7464  prcdnql  7486  prcunqu  7487  nn0ge2m1nn  9239  nn0le2is012  9338  fzind  9371  nn0ind-raph  9373  zindd  9374  uzin  9563  indstr  9596  xnn0xadd0  9870  icoshft  9993  fzen  10046  uzsubsubfz  10050  elfz1b  10093  elfz0ubfz0  10128  elfz0fzfz0  10129  fz0fzelfz0  10130  elfzmlbp  10135  elfzodifsumelfzo  10204  ssfzo12bi  10228  elfzonelfzo  10233  modfzo0difsn  10398  frec2uzuzd  10405  expcllem  10534  mulexp  10562  leexp2r  10577  bernneq  10644  facdiv  10721  cjexp  10905  absexp  11091  clim2prod  11550  prodfap0  11556  prodfrecap  11557  prodmodc  11589  fprodabs  11627  addmodlteqALT  11868  oddge22np1  11889  nn0enne  11910  nn0o1gt2  11913  gcdneg  11986  dfgcd2  12018  rplpwr  12031  coprmdvds1  12094  qredeq  12099  cncongr1  12106  cncongr2  12107  prm2orodd  12129  nnnn0modprm0  12258  prm23lt5  12266  dvdsprmpweqnn  12338  dvdsprmpweqle  12339  oddprmdvds  12355  prmpwdvds  12356  setsn0fun  12502  isnmgm  12786  sgrpass  12821  insubm  12879  dfgrp3mlem  12975  fiinopn  13665  tgcl  13725  distop  13746  ssnei2  13818  tgcnp  13870  cnpnei  13880  cnmptcom  13959  neibl  14152  zabsle1  14561  bj-nnbist  14657  sumdc2  14712