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  6531  tpossym  6551  ercnv  6832  cnvct  7101  php5dom  7168  3xpfi  7245  recrecnq  7767  1idpr  7965  eqlei2  8427  lem1  9185  eluzfz1  10452  fzpred  10494  uznfz  10527  fz0fzdiffz0  10554  fzctr  10557  flid  10740  flqeqceilz  10776  faclbnd3  11203  bcn1  11218  isfinite4im  11253  hashfac  11310  leabs  11862  gcd0id  12781  lcmgcdlem  12880  dvdsnprmd  12928  pcprod  13154  fldivp1  13156  intopsn  13746  mgm1  13749  sgrp1  13785  mnd1  13821  mnd1id  13822  grp1  13970  grp1inv  13971  eqger  14086  eqgid  14088  qusghm  14144  cntzrcl  14159  rngressid  14360  ring1  14471  ringressid  14477  subrgsubm  14651  resrhm2b  14666  lssex  14800  cncrng  15015  ressascl  15148  psrbagfsupp  15164  psrbaglesupp  15167  eltpsg  15266  tg1  15285  cldval  15325  cldss  15331  cldopn  15333  psmetdmdm  15550  dvef  15953  relogef  16093  bposlem7  16317  zabsle1  16323  usgredg2vlem2  16669  wlkprop  16773  wlkvtxiedg  16791  eupthseg  16898  bj-nn0suc0  17181