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  443  pm2.24  611  con3rr3  623  expt  647  mtt  675  jaod  707  orel1  715  pm2.62  738  pm2.64  791  pm2.75  799  pm2.61ddc  847  peircedc  900  dcbi  921  pm5.62dc  930  pm4.83dc  936  ccased  950  3impd  1200  3expd  1203  mp3an1i  1309  pclem6  1353  simplbi2com  1421  19.21ht  1561  19.33b2  1609  equtrr  1687  spimeh  1718  cbv1  1723  equvini  1732  sbequ2  1743  ax11e  1769  ax11b  1799  sb6rf  1826  sb56  1858  exmoeudc  2063  moimv  2066  eupickbi  2082  exists2  2097  r19.12  2541  2gencl  2722  3gencl  2723  rspccv  2790  ceqex  2816  mo2icl  2867  mob  2870  euind  2875  reuind  2893  sseq2  3126  nelss  3163  difin  3318  reupick2  3367  uneqdifeqim  3453  difsn  3665  sssnm  3689  preq12b  3705  iinss2  3873  trintssm  4050  sspwb  4146  copsexg  4174  pocl  4233  pofun  4242  sowlin  4250  reusv1  4387  alxfr  4390  ralxfrALT  4396  iunpw  4409  onsucelsucr  4432  reg2exmidlema  4457  en2lp  4477  2optocl  4624  3optocl  4625  ssrel  4635  ssrel2  4637  ssrelrel  4647  relop  4697  xpidtr  4937  trin2  4938  poltletr  4947  xp11m  4985  relcnvtr  5066  iotaval  5107  funmo  5146  fss  5292  f0dom0  5324  fv3  5452  tz6.12c  5459  mpteqb  5519  funfvima  5657  f1veqaeq  5678  isoselem  5729  oprabid  5811  ovg  5917  fornex  6021  f1o2ndf1  6133  poxp  6137  tposfn2  6171  smoel  6205  tfri3  6272  nnaass  6389  nnmordi  6420  iinerm  6509  2ecoptocl  6525  3ecoptocl  6526  th3qlem2  6540  enm  6722  xpdom2  6733  xpf1o  6746  findcard2  6791  findcard2s  6792  eldju2ndl  6965  updjud  6975  distrnq0  7291  addassnq0  7294  prcdnql  7316  prcunqu  7317  nn0ge2m1nn  9061  nn0le2is012  9157  fzind  9190  nn0ind-raph  9192  zindd  9193  uzin  9382  indstr  9415  xnn0xadd0  9680  icoshft  9803  fzen  9854  uzsubsubfz  9858  elfz1b  9901  elfz0ubfz0  9933  elfz0fzfz0  9934  fz0fzelfz0  9935  elfzmlbp  9940  elfzodifsumelfzo  10009  ssfzo12bi  10033  elfzonelfzo  10038  modfzo0difsn  10199  frec2uzuzd  10206  expcllem  10335  mulexp  10363  leexp2r  10378  bernneq  10443  facdiv  10516  cjexp  10697  absexp  10883  clim2prod  11340  prodfap0  11346  prodfrecap  11347  prodmodc  11379  addmodlteqALT  11593  oddge22np1  11614  nn0enne  11635  nn0o1gt2  11638  gcdneg  11706  dfgcd2  11738  rplpwr  11751  coprmdvds1  11808  qredeq  11813  cncongr1  11820  cncongr2  11821  prm2orodd  11843  setsn0fun  12035  fiinopn  12210  tgcl  12272  distop  12293  ssnei2  12365  tgcnp  12417  cnpnei  12427  cnmptcom  12506  neibl  12699  bj-nnbist  13124  sumdc2  13177