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  98  expcom  115  impcom  124  syl5ibcom  154  syl5ibrcom  156  pm5.501  243  impd  252  expd  256  pm3.21  262  imdistanri  442  pm2.24  610  con3rr3  622  expt  646  mtt  674  jaod  706  orel1  714  pm2.62  737  pm2.64  790  pm2.75  798  pm2.61ddc  846  peircedc  899  dcbi  920  pm5.62dc  929  pm4.83dc  935  ccased  949  3impd  1199  3expd  1202  mp3an1i  1308  pclem6  1352  simplbi2com  1420  19.21ht  1560  19.33b2  1608  equtrr  1686  spimeh  1717  cbv1  1722  equvini  1731  sbequ2  1742  ax11e  1768  ax11b  1798  sb6rf  1825  sb56  1857  exmoeudc  2062  moimv  2065  eupickbi  2081  exists2  2096  r19.12  2538  2gencl  2719  3gencl  2720  rspccv  2786  ceqex  2812  mo2icl  2863  mob  2866  euind  2871  reuind  2889  sseq2  3121  nelss  3158  difin  3313  reupick2  3362  uneqdifeqim  3448  difsn  3657  sssnm  3681  preq12b  3697  iinss2  3865  trintssm  4042  sspwb  4138  copsexg  4166  pocl  4225  pofun  4234  sowlin  4242  reusv1  4379  alxfr  4382  ralxfrALT  4388  iunpw  4401  onsucelsucr  4424  reg2exmidlema  4449  en2lp  4469  2optocl  4616  3optocl  4617  ssrel  4627  ssrel2  4629  ssrelrel  4639  relop  4689  xpidtr  4929  trin2  4930  poltletr  4939  xp11m  4977  relcnvtr  5058  iotaval  5099  funmo  5138  fss  5284  f0dom0  5316  fv3  5444  tz6.12c  5451  mpteqb  5511  funfvima  5649  f1veqaeq  5670  isoselem  5721  oprabid  5803  ovg  5909  fornex  6013  f1o2ndf1  6125  poxp  6129  tposfn2  6163  smoel  6197  tfri3  6264  nnaass  6381  nnmordi  6412  iinerm  6501  2ecoptocl  6517  3ecoptocl  6518  th3qlem2  6532  enm  6714  xpdom2  6725  xpf1o  6738  findcard2  6783  findcard2s  6784  eldju2ndl  6957  updjud  6967  distrnq0  7267  addassnq0  7270  prcdnql  7292  prcunqu  7293  nn0ge2m1nn  9037  nn0le2is012  9133  fzind  9166  nn0ind-raph  9168  zindd  9169  uzin  9358  indstr  9388  xnn0xadd0  9650  icoshft  9773  fzen  9823  uzsubsubfz  9827  elfz1b  9870  elfz0ubfz0  9902  elfz0fzfz0  9903  fz0fzelfz0  9904  elfzmlbp  9909  elfzodifsumelfzo  9978  ssfzo12bi  10002  elfzonelfzo  10007  modfzo0difsn  10168  frec2uzuzd  10175  expcllem  10304  mulexp  10332  leexp2r  10347  bernneq  10412  facdiv  10484  cjexp  10665  absexp  10851  clim2prod  11308  prodfap0  11314  prodfrecap  11315  prodmodc  11347  addmodlteqALT  11557  oddge22np1  11578  nn0enne  11599  nn0o1gt2  11602  gcdneg  11670  dfgcd2  11702  rplpwr  11715  coprmdvds1  11772  qredeq  11777  cncongr1  11784  cncongr2  11785  prm2orodd  11807  setsn0fun  11996  fiinopn  12171  tgcl  12233  distop  12254  ssnei2  12326  tgcnp  12378  cnpnei  12388  cnmptcom  12467  neibl  12660  bj-nnbist  12953  sumdc2  13006