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  626  con3rr3  638  expt  663  mtt  692  jaod  725  orel1  733  pm2.62  756  pm2.64  809  pm2.75  817  pm2.61ddc  869  peircedc  922  dcbi  945  pm5.62dc  954  pm4.83dc  960  ccased  974  3impd  1248  3expd  1251  syldbl2  1329  mp3an1i  1367  pclem6  1419  simplbi2com  1490  19.21ht  1630  19.33b2  1678  equtrr  1758  spimeh  1787  cbv1  1793  cbv1v  1795  equvini  1806  sbequ2  1817  ax11e  1844  ax11b  1874  sb6rf  1901  sb56  1934  exmoeudc  2143  moimv  2146  eupickbi  2162  exists2  2177  r19.12  2640  2gencl  2837  3gencl  2838  vtocl4ga  2877  rspccv  2908  ceqex  2934  mo2icl  2986  mob  2989  euind  2994  reuind  3012  sseq2  3252  nelss  3289  difin  3446  reupick2  3495  uneqdifeqim  3582  difsn  3815  ssprsseq  3840  sssnm  3842  preq12b  3858  iinss2  4028  trintssm  4208  sspwb  4314  copsexg  4342  pocl  4406  pofun  4415  sowlin  4423  reusv1  4561  alxfr  4564  ralxfrALT  4570  iunpw  4583  onsucelsucr  4612  reg2exmidlema  4638  en2lp  4658  2optocl  4809  3optocl  4810  ssrel  4820  ssrel2  4822  ssrelrel  4832  relop  4886  xpidtr  5134  trin2  5135  poltletr  5144  xp11m  5182  relcnvtr  5263  iotaval  5305  funmo  5348  fundif  5381  fss  5501  f0dom0  5539  fv3  5671  tz6.12c  5678  mpteqb  5746  funfvima  5896  f1veqaeq  5920  isoselem  5971  oprabid  6060  ovg  6171  focdmex  6286  f1o2ndf1  6402  poxp  6406  tposfn2  6475  smoel  6509  tfri3  6576  nnaass  6696  nnmordi  6727  iinerm  6819  2ecoptocl  6835  3ecoptocl  6836  th3qlem2  6850  enm  7047  xpdom2  7058  xpf1o  7073  findcard2  7121  findcard2s  7122  eldju2ndl  7314  updjud  7324  nninfninc  7365  distrnq0  7722  addassnq0  7725  prcdnql  7747  prcunqu  7748  nn0ge2m1nn  9506  nn0le2is012  9606  fzind  9639  nn0ind-raph  9641  zindd  9642  uzin  9833  indstr  9871  xnn0xadd0  10146  icoshft  10269  fzen  10323  uzsubsubfz  10327  elfz1b  10370  elfz0ubfz0  10405  elfz0fzfz0  10406  fz0fzelfz0  10407  elfzmlbp  10412  elfzodifsumelfzo  10492  ssfzo12bi  10516  elfzonelfzo  10521  modfzo0difsn  10703  frec2uzuzd  10710  expcllem  10858  mulexp  10886  leexp2r  10901  bernneq  10968  facdiv  11046  fundm2domnop0  11158  ccatsymb  11228  swrdnd  11289  swrdswrdlem  11334  swrdswrd  11335  pfxccatin12lem2a  11357  pfxccatin12lem1  11358  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12lem3  11362  pfxccat3  11364  swrdccat  11365  swrdccat3blem  11369  cjexp  11516  absexp  11702  clim2prod  12163  prodfap0  12169  prodfrecap  12170  prodmodc  12202  fprodabs  12240  addmodlteqALT  12483  oddge22np1  12505  nn0enne  12526  nn0o1gt2  12529  gcdneg  12616  dfgcd2  12648  rplpwr  12661  coprmdvds1  12726  qredeq  12731  cncongr1  12738  cncongr2  12739  prm2orodd  12761  nnnn0modprm0  12891  prm23lt5  12899  dvdsprmpweqnn  12972  dvdsprmpweqle  12973  oddprmdvds  12990  prmpwdvds  12991  setsn0fun  13182  isnmgm  13506  sgrpass  13554  insubm  13631  dfgrp3mlem  13744  fiinopn  14798  tgcl  14858  distop  14879  ssnei2  14951  tgcnp  15003  cnpnei  15013  cnmptcom  15092  neibl  15285  rpcxpmul2  15707  fsumdvdsmul  15788  zabsle1  15801  gausslemma2dlem1a  15860  gausslemma2dlem3  15865  lgsquad2lem2  15884  2lgs  15906  umgrnloop  16040  upgrpredgv  16070  upgredgpr  16073  wlkl1loop  16282  upgriswlkdc  16284  upgrwlkvtxedg  16288  uspgr2wlkeq  16289  wlkv0  16293  wlkres  16303  clwwlkccatlem  16324  loopclwwlkn1b  16343  umgr2cwwk2dif  16348  clwwlknonex2lem2  16362  clwwlknonex2  16363  eupth2lem3lem4fi  16397  depindlem2  16431  bj-nnbist  16445  sumdc2  16500