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  mp3an1i  1341  pclem6  1385  simplbi2com  1455  19.21ht  1592  19.33b2  1640  equtrr  1721  spimeh  1750  cbv1  1756  cbv1v  1758  equvini  1769  sbequ2  1780  ax11e  1807  ax11b  1837  sb6rf  1864  sb56  1897  exmoeudc  2105  moimv  2108  eupickbi  2124  exists2  2139  r19.12  2600  2gencl  2793  3gencl  2794  rspccv  2861  ceqex  2887  mo2icl  2939  mob  2942  euind  2947  reuind  2965  sseq2  3203  nelss  3240  difin  3396  reupick2  3445  uneqdifeqim  3532  difsn  3755  sssnm  3780  preq12b  3796  iinss2  3965  trintssm  4143  sspwb  4245  copsexg  4273  pocl  4334  pofun  4343  sowlin  4351  reusv1  4489  alxfr  4492  ralxfrALT  4498  iunpw  4511  onsucelsucr  4540  reg2exmidlema  4566  en2lp  4586  2optocl  4736  3optocl  4737  ssrel  4747  ssrel2  4749  ssrelrel  4759  relop  4812  xpidtr  5056  trin2  5057  poltletr  5066  xp11m  5104  relcnvtr  5185  iotaval  5226  funmo  5269  fss  5415  f0dom0  5447  fv3  5577  tz6.12c  5584  mpteqb  5648  funfvima  5790  f1veqaeq  5812  isoselem  5863  oprabid  5950  ovg  6057  focdmex  6167  f1o2ndf1  6281  poxp  6285  tposfn2  6319  smoel  6353  tfri3  6420  nnaass  6538  nnmordi  6569  iinerm  6661  2ecoptocl  6677  3ecoptocl  6678  th3qlem2  6692  enm  6874  xpdom2  6885  xpf1o  6900  findcard2  6945  findcard2s  6946  eldju2ndl  7131  updjud  7141  nninfninc  7182  distrnq0  7519  addassnq0  7522  prcdnql  7544  prcunqu  7545  nn0ge2m1nn  9300  nn0le2is012  9399  fzind  9432  nn0ind-raph  9434  zindd  9435  uzin  9625  indstr  9658  xnn0xadd0  9933  icoshft  10056  fzen  10109  uzsubsubfz  10113  elfz1b  10156  elfz0ubfz0  10191  elfz0fzfz0  10192  fz0fzelfz0  10193  elfzmlbp  10198  elfzodifsumelfzo  10268  ssfzo12bi  10292  elfzonelfzo  10297  modfzo0difsn  10466  frec2uzuzd  10473  expcllem  10621  mulexp  10649  leexp2r  10664  bernneq  10731  facdiv  10809  cjexp  11037  absexp  11223  clim2prod  11682  prodfap0  11688  prodfrecap  11689  prodmodc  11721  fprodabs  11759  addmodlteqALT  12001  oddge22np1  12022  nn0enne  12043  nn0o1gt2  12046  gcdneg  12119  dfgcd2  12151  rplpwr  12164  coprmdvds1  12229  qredeq  12234  cncongr1  12241  cncongr2  12242  prm2orodd  12264  nnnn0modprm0  12393  prm23lt5  12401  dvdsprmpweqnn  12474  dvdsprmpweqle  12475  oddprmdvds  12492  prmpwdvds  12493  setsn0fun  12655  isnmgm  12943  sgrpass  12991  insubm  13057  dfgrp3mlem  13170  fiinopn  14172  tgcl  14232  distop  14253  ssnei2  14325  tgcnp  14377  cnpnei  14387  cnmptcom  14466  neibl  14659  zabsle1  15115  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  bj-nnbist  15236  sumdc2  15291