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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  450  pm2.24  630  con3rr3  642  expt  667  mtt  696  jaod  729  orel1  737  pm2.62  760  pm2.64  813  pm2.75  821  pm2.61ddc  873  peircedc  926  dcbi  949  pm5.62dc  958  pm4.83dc  964  ccased  978  3impd  1252  3expd  1255  syldbl2  1333  mp3an1i  1371  pclem6  1423  simplbi2com  1494  19.21ht  1634  19.33b2  1682  equtrr  1762  spimeh  1792  cbv1  1798  cbv1v  1800  equvini  1811  sbequ2  1822  ax11e  1849  ax11b  1879  sb6rf  1906  sb56  1940  exmoeudc  2150  moimv  2153  eupickbi  2169  exists2  2184  r19.12  2657  2gencl  2855  3gencl  2856  vtocl4ga  2895  rspccv  2926  ceqex  2953  mo2icl  3005  mob  3008  euind  3013  reuind  3031  sseq2  3272  nelss  3309  difin  3468  reupick2  3519  uneqdifeqim  3613  sspw  3702  difsn  3852  ssprsseq  3877  sssnm  3879  preq12b  3895  iinss2  4065  trintssm  4247  sspwb  4358  copsexg  4386  pocl  4450  pofun  4459  sowlin  4467  reusv1  4606  alxfr  4609  ralxfrALT  4615  iunpw  4628  onsucelsucr  4657  reg2exmidlema  4683  en2lp  4703  2optocl  4854  3optocl  4855  ssrel  4865  ssrel2  4867  ssrelrel  4877  relop  4932  xpidtr  5181  trin2  5182  poltletr  5191  xp11m  5229  relcnvtr  5310  iotaval  5352  funmo  5395  fundif  5428  fss  5549  f0dom0  5589  fv3  5721  tz6.12c  5728  mpteqb  5799  funfvima  5953  f1veqaeq  5978  isoselem  6029  oprabid  6120  ovg  6231  focdmex  6348  f1o2ndf1  6468  poxp  6472  tposfn2  6542  smoel  6576  tfri3  6643  nnaass  6763  nnmordi  6794  iinerm  6886  2ecoptocl  6902  3ecoptocl  6903  th3qlem2  6917  enm  7124  xpdom2  7135  xpf1o  7150  findcard2  7199  findcard2s  7200  eldju2ndl  7418  updjud  7428  nninfninc  7469  distrnq0  7832  addassnq0  7835  prcdnql  7857  prcunqu  7858  nn0ge2m1nn  9636  nn0le2is012  9737  fzind  9771  nn0ind-raph  9773  zindd  9774  uzin  9970  indstr  10008  xnn0xadd0  10285  icoshft  10408  fzen  10463  uzsubsubfz  10468  elfz1b  10513  elfz0ubfz0  10548  elfz0fzfz0  10549  fz0fzelfz0  10550  elfzmlbp  10555  elfzodifsumelfzo  10635  ssfzo12bi  10659  elfzonelfzo  10664  modfzo0difsn  10852  frec2uzuzd  10859  expcllem  11007  mulexp  11035  leexp2r  11050  bernneq  11118  facdiv  11197  fundm2domnop0  11321  ccatsymb  11391  swrdnd  11452  swrdswrdlem  11497  swrdswrd  11498  pfxccatin12lem2a  11520  pfxccatin12lem1  11521  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccat3  11527  swrdccat  11528  swrdccat3blem  11532  cjexp  11679  absexp  11867  clim2prod  12330  prodfap0  12336  prodfrecap  12337  prodmodc  12369  fprodabs  12407  addmodlteqALT  12650  oddge22np1  12672  nn0enne  12693  nn0o1gt2  12696  gcdneg  12783  dfgcd2  12815  rplpwr  12828  coprmdvds1  12893  qredeq  12898  cncongr1  12905  cncongr2  12906  prm2orodd  12928  nnnn0modprm0  13062  prm23lt5  13070  dvdsprmpweqnn  13143  dvdsprmpweqle  13144  oddprmdvds  13161  prmpwdvds  13162  setsn0fun  13446  isnmgm  13738  sgrpass  13781  insubm  13850  dfgrp3mlem  13961  fiinopn  15247  tgcl  15307  distop  15328  ssnei2  15400  tgcnp  15452  cnpnei  15462  cnmptcom  15541  neibl  15734  rpcxpmul2  16163  fsumdvdsmul  16302  zabsle1  16340  gausslemma2dlem1a  16399  gausslemma2dlem3  16404  lgsquad2lem2  16423  2lgs  16445  umgrnloop  16579  upgrpredgv  16609  upgredgpr  16612  wlkl1loop  16821  upgriswlkdc  16823  upgrwlkvtxedg  16827  uspgr2wlkeq  16828  wlkv0  16832  wlkres  16842  clwwlkccatlem  16863  loopclwwlkn1b  16882  umgr2cwwk2dif  16887  clwwlknonex2lem2  16901  clwwlknonex2  16902  eupth2lem3lem4fi  16936  depindlem2  16970  bj-nnbist  16994  sumdc2  17049