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  4655  sucunielr  4657  ordsuc  4710  peano2b  4762  xpiindim  4917  fununfun  5424  fvelrnb  5750  fliftcnv  6001  riotaprop  6064  unielxp  6408  dmtpos  6527  tpossym  6547  ercnv  6828  cnvct  7097  php5dom  7164  3xpfi  7241  recrecnq  7762  1idpr  7960  eqlei2  8422  lem1  9180  eluzfz1  10446  fzpred  10488  uznfz  10521  fz0fzdiffz0  10548  fzctr  10551  flid  10734  flqeqceilz  10770  faclbnd3  11197  bcn1  11212  isfinite4im  11247  hashfac  11304  leabs  11856  gcd0id  12775  lcmgcdlem  12874  dvdsnprmd  12922  pcprod  13148  fldivp1  13150  intopsn  13740  mgm1  13743  sgrp1  13779  mnd1  13815  mnd1id  13816  grp1  13964  grp1inv  13965  eqger  14080  eqgid  14082  qusghm  14138  cntzrcl  14153  rngressid  14337  ring1  14448  ringressid  14452  subrgsubm  14626  resrhm2b  14641  lssex  14775  cncrng  14990  ressascl  15123  psrbagfsupp  15139  psrbaglesupp  15142  eltpsg  15232  tg1  15251  cldval  15291  cldss  15297  cldopn  15299  psmetdmdm  15516  dvef  15919  relogef  16057  bposlem7  16278  zabsle1  16284  usgredg2vlem2  16630  wlkprop  16734  wlkvtxiedg  16752  eupthseg  16859  bj-nn0suc0  17142