Theorem mpancom 419

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 409	1 |- ( ps -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpan  421  spesbc  3036  onsucelsucr  4485  sucunielr  4487  ordsuc  4540  peano2b  4592  xpiindim  4741  fvelrnb  5534  fliftcnv  5763  riotaprop  5821  unielxp  6142  dmtpos  6224  tpossym  6244  ercnv  6522  cnvct  6775  php5dom  6829  3xpfi  6896  recrecnq  7335  1idpr  7533  eqlei2  7993  lem1  8742  eluzfz1  9966  fzpred  10005  uznfz  10038  fz0fzdiffz0  10065  fzctr  10068  flid  10219  flqeqceilz  10253  faclbnd3  10656  bcn1  10671  isfinite4im  10706  leabs  11016  gcd0id  11912  lcmgcdlem  12009  dvdsnprmd  12057  pcprod  12276  fldivp1  12278  intopsn  12598  mgm1  12601  eltpsg  12678  tg1  12699  cldval  12739  cldss  12745  cldopn  12747  psmetdmdm  12964  dvef  13328  relogef  13425  zabsle1  13540  bj-nn0suc0  13832