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  3084  onsucelsucr  4556  sucunielr  4558  ordsuc  4611  peano2b  4663  xpiindim  4815  fununfun  5317  fvelrnb  5626  fliftcnv  5864  riotaprop  5923  unielxp  6260  dmtpos  6342  tpossym  6362  ercnv  6641  cnvct  6901  php5dom  6960  3xpfi  7030  recrecnq  7507  1idpr  7705  eqlei2  8167  lem1  8920  eluzfz1  10153  fzpred  10192  uznfz  10225  fz0fzdiffz0  10252  fzctr  10255  flid  10427  flqeqceilz  10463  faclbnd3  10888  bcn1  10903  isfinite4im  10937  leabs  11385  gcd0id  12300  lcmgcdlem  12399  dvdsnprmd  12447  pcprod  12669  fldivp1  12671  intopsn  13199  mgm1  13202  sgrp1  13243  mnd1  13287  mnd1id  13288  grp1  13438  grp1inv  13439  eqger  13560  eqgid  13562  qusghm  13618  rngressid  13716  ring1  13821  ringressid  13825  subrgsubm  13996  resrhm2b  14011  lssex  14116  cncrng  14331  eltpsg  14512  tg1  14531  cldval  14571  cldss  14577  cldopn  14579  psmetdmdm  14796  dvef  15199  relogef  15336  zabsle1  15476  bj-nn0suc0  15886