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  1595  19.33b2  1643  equtrr  1724  spimeh  1753  cbv1  1759  cbv1v  1761  equvini  1772  sbequ2  1783  ax11e  1810  ax11b  1840  sb6rf  1867  sb56  1900  exmoeudc  2108  moimv  2111  eupickbi  2127  exists2  2142  r19.12  2603  2gencl  2796  3gencl  2797  rspccv  2865  ceqex  2891  mo2icl  2943  mob  2946  euind  2951  reuind  2969  sseq2  3207  nelss  3244  difin  3400  reupick2  3449  uneqdifeqim  3536  difsn  3759  sssnm  3784  preq12b  3800  iinss2  3969  trintssm  4147  sspwb  4249  copsexg  4277  pocl  4338  pofun  4347  sowlin  4355  reusv1  4493  alxfr  4496  ralxfrALT  4502  iunpw  4515  onsucelsucr  4544  reg2exmidlema  4570  en2lp  4590  2optocl  4740  3optocl  4741  ssrel  4751  ssrel2  4753  ssrelrel  4763  relop  4816  xpidtr  5060  trin2  5061  poltletr  5070  xp11m  5108  relcnvtr  5189  iotaval  5230  funmo  5273  fss  5419  f0dom0  5451  fv3  5581  tz6.12c  5588  mpteqb  5652  funfvima  5794  f1veqaeq  5816  isoselem  5867  oprabid  5954  ovg  6062  focdmex  6172  f1o2ndf1  6286  poxp  6290  tposfn2  6324  smoel  6358  tfri3  6425  nnaass  6543  nnmordi  6574  iinerm  6666  2ecoptocl  6682  3ecoptocl  6683  th3qlem2  6697  enm  6879  xpdom2  6890  xpf1o  6905  findcard2  6950  findcard2s  6951  eldju2ndl  7138  updjud  7148  nninfninc  7189  distrnq0  7526  addassnq0  7529  prcdnql  7551  prcunqu  7552  nn0ge2m1nn  9309  nn0le2is012  9408  fzind  9441  nn0ind-raph  9443  zindd  9444  uzin  9634  indstr  9667  xnn0xadd0  9942  icoshft  10065  fzen  10118  uzsubsubfz  10122  elfz1b  10165  elfz0ubfz0  10200  elfz0fzfz0  10201  fz0fzelfz0  10202  elfzmlbp  10207  elfzodifsumelfzo  10277  ssfzo12bi  10301  elfzonelfzo  10306  modfzo0difsn  10487  frec2uzuzd  10494  expcllem  10642  mulexp  10670  leexp2r  10685  bernneq  10752  facdiv  10830  cjexp  11058  absexp  11244  clim2prod  11704  prodfap0  11710  prodfrecap  11711  prodmodc  11743  fprodabs  11781  addmodlteqALT  12024  oddge22np1  12046  nn0enne  12067  nn0o1gt2  12070  gcdneg  12149  dfgcd2  12181  rplpwr  12194  coprmdvds1  12259  qredeq  12264  cncongr1  12271  cncongr2  12272  prm2orodd  12294  nnnn0modprm0  12424  prm23lt5  12432  dvdsprmpweqnn  12505  dvdsprmpweqle  12506  oddprmdvds  12523  prmpwdvds  12524  setsn0fun  12715  isnmgm  13003  sgrpass  13051  insubm  13117  dfgrp3mlem  13230  fiinopn  14240  tgcl  14300  distop  14321  ssnei2  14393  tgcnp  14445  cnpnei  14455  cnmptcom  14534  neibl  14727  rpcxpmul2  15149  fsumdvdsmul  15227  zabsle1  15240  gausslemma2dlem1a  15299  gausslemma2dlem3  15304  lgsquad2lem2  15323  2lgs  15345  bj-nnbist  15390  sumdc2  15445