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  621  con3rr3  633  expt  657  mtt  685  jaod  717  orel1  725  pm2.62  748  pm2.64  801  pm2.75  809  pm2.61ddc  861  peircedc  914  dcbi  936  pm5.62dc  945  pm4.83dc  951  ccased  965  3impd  1221  3expd  1224  mp3an1i  1330  pclem6  1374  simplbi2com  1444  19.21ht  1581  19.33b2  1629  equtrr  1710  spimeh  1739  cbv1  1745  cbv1v  1747  equvini  1758  sbequ2  1769  ax11e  1796  ax11b  1826  sb6rf  1853  sb56  1885  exmoeudc  2089  moimv  2092  eupickbi  2108  exists2  2123  r19.12  2583  2gencl  2771  3gencl  2772  rspccv  2839  ceqex  2865  mo2icl  2917  mob  2920  euind  2925  reuind  2943  sseq2  3180  nelss  3217  difin  3373  reupick2  3422  uneqdifeqim  3509  difsn  3730  sssnm  3755  preq12b  3771  iinss2  3940  trintssm  4118  sspwb  4217  copsexg  4245  pocl  4304  pofun  4313  sowlin  4321  reusv1  4459  alxfr  4462  ralxfrALT  4468  iunpw  4481  onsucelsucr  4508  reg2exmidlema  4534  en2lp  4554  2optocl  4704  3optocl  4705  ssrel  4715  ssrel2  4717  ssrelrel  4727  relop  4778  xpidtr  5020  trin2  5021  poltletr  5030  xp11m  5068  relcnvtr  5149  iotaval  5190  funmo  5232  fss  5378  f0dom0  5410  fv3  5539  tz6.12c  5546  mpteqb  5607  funfvima  5749  f1veqaeq  5770  isoselem  5821  oprabid  5907  ovg  6013  focdmex  6116  f1o2ndf1  6229  poxp  6233  tposfn2  6267  smoel  6301  tfri3  6368  nnaass  6486  nnmordi  6517  iinerm  6607  2ecoptocl  6623  3ecoptocl  6624  th3qlem2  6638  enm  6820  xpdom2  6831  xpf1o  6844  findcard2  6889  findcard2s  6890  eldju2ndl  7071  updjud  7081  distrnq0  7458  addassnq0  7461  prcdnql  7483  prcunqu  7484  nn0ge2m1nn  9236  nn0le2is012  9335  fzind  9368  nn0ind-raph  9370  zindd  9371  uzin  9560  indstr  9593  xnn0xadd0  9867  icoshft  9990  fzen  10043  uzsubsubfz  10047  elfz1b  10090  elfz0ubfz0  10125  elfz0fzfz0  10126  fz0fzelfz0  10127  elfzmlbp  10132  elfzodifsumelfzo  10201  ssfzo12bi  10225  elfzonelfzo  10230  modfzo0difsn  10395  frec2uzuzd  10402  expcllem  10531  mulexp  10559  leexp2r  10574  bernneq  10641  facdiv  10718  cjexp  10902  absexp  11088  clim2prod  11547  prodfap0  11553  prodfrecap  11554  prodmodc  11586  fprodabs  11624  addmodlteqALT  11865  oddge22np1  11886  nn0enne  11907  nn0o1gt2  11910  gcdneg  11983  dfgcd2  12015  rplpwr  12028  coprmdvds1  12091  qredeq  12096  cncongr1  12103  cncongr2  12104  prm2orodd  12126  nnnn0modprm0  12255  prm23lt5  12263  dvdsprmpweqnn  12335  dvdsprmpweqle  12336  oddprmdvds  12352  prmpwdvds  12353  setsn0fun  12499  isnmgm  12779  sgrpass  12814  insubm  12872  dfgrp3mlem  12968  fiinopn  13507  tgcl  13567  distop  13588  ssnei2  13660  tgcnp  13712  cnpnei  13722  cnmptcom  13801  neibl  13994  zabsle1  14403  bj-nnbist  14499  sumdc2  14554