Theorem mpancom 426

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpan  428  spesbc  3138  onsucelsucr  4657  sucunielr  4659  ordsuc  4712  peano2b  4764  xpiindim  4919  fununfun  5427  fvelrnb  5753  fliftcnv  6004  riotaprop  6067  unielxp  6412  dmtpos  6532  tpossym  6552  ercnv  6833  cnvct  7103  php5dom  7170  3xpfi  7247  recrecnq  7767  1idpr  7965  eqlei2  8427  lem1  9185  eluzfz1  10451  fzpred  10493  uznfz  10526  fz0fzdiffz0  10553  fzctr  10556  flid  10739  flqeqceilz  10775  faclbnd3  11202  bcn1  11217  isfinite4im  11252  hashfac  11309  leabs  11861  gcd0id  12780  lcmgcdlem  12879  dvdsnprmd  12927  pcprod  13153  fldivp1  13155  intopsn  13745  mgm1  13748  sgrp1  13784  mnd1  13820  mnd1id  13821  grp1  13969  grp1inv  13970  eqger  14085  eqgid  14087  qusghm  14143  cntzrcl  14158  rngressid  14359  ring1  14470  ringressid  14476  subrgsubm  14650  resrhm2b  14665  lssex  14799  cncrng  15014  ressascl  15147  psrbaglesupp  15171  eltpsg  15283  tg1  15302  cldval  15342  cldss  15348  cldopn  15350  psmetdmdm  15567  dvef  15970  relogef  16110  bposlem7  16334  zabsle1  16340  usgredg2vlem2  16686  wlkprop  16790  wlkvtxiedg  16808  eupthseg  16915  bj-nn0suc0  17198