Theorem mpancom 422

Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpancom.1	|- ( ps -> ph )
mpancom.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mpancom	|- ( ps -> ch )

Proof of Theorem mpancom

Step	Hyp	Ref	Expression
1		mpancom.1	. 2 |- ( ps -> ph )
2		id 19	. 2 |- ( ps -> ps )
3		mpancom.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	1, 2, 3	syl2anc 411	1 |- ( ps -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mpan  424  spesbc  3092  onsucelsucr  4574  sucunielr  4576  ordsuc  4629  peano2b  4681  xpiindim  4833  fununfun  5336  fvelrnb  5649  fliftcnv  5887  riotaprop  5946  unielxp  6283  dmtpos  6365  tpossym  6385  ercnv  6664  cnvct  6925  php5dom  6985  3xpfi  7056  recrecnq  7542  1idpr  7740  eqlei2  8202  lem1  8955  eluzfz1  10188  fzpred  10227  uznfz  10260  fz0fzdiffz0  10287  fzctr  10290  flid  10464  flqeqceilz  10500  faclbnd3  10925  bcn1  10940  isfinite4im  10974  leabs  11500  gcd0id  12415  lcmgcdlem  12514  dvdsnprmd  12562  pcprod  12784  fldivp1  12786  intopsn  13314  mgm1  13317  sgrp1  13358  mnd1  13402  mnd1id  13403  grp1  13553  grp1inv  13554  eqger  13675  eqgid  13677  qusghm  13733  rngressid  13831  ring1  13936  ringressid  13940  subrgsubm  14111  resrhm2b  14126  lssex  14231  cncrng  14446  eltpsg  14627  tg1  14646  cldval  14686  cldss  14692  cldopn  14694  psmetdmdm  14911  dvef  15314  relogef  15451  zabsle1  15591  bj-nn0suc0  16085