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 )

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  428  spesbc  3138  onsucelsucr  4650  sucunielr  4652  ordsuc  4705  peano2b  4757  xpiindim  4912  fununfun  5419  fvelrnb  5744  fliftcnv  5991  riotaprop  6054  unielxp  6398  dmtpos  6517  tpossym  6537  ercnv  6818  cnvct  7087  php5dom  7154  3xpfi  7231  recrecnq  7751  1idpr  7949  eqlei2  8410  lem1  9167  eluzfz1  10414  fzpred  10455  uznfz  10488  fz0fzdiffz0  10515  fzctr  10518  flid  10697  flqeqceilz  10733  faclbnd3  11159  bcn1  11174  isfinite4im  11209  hashfac  11266  leabs  11818  gcd0id  12734  lcmgcdlem  12833  dvdsnprmd  12881  pcprod  13103  fldivp1  13105  intopsn  13664  mgm1  13667  sgrp1  13703  mnd1  13739  mnd1id  13740  grp1  13888  grp1inv  13889  eqger  14004  eqgid  14006  qusghm  14062  rngressid  14228  ring1  14337  ringressid  14341  subrgsubm  14515  resrhm2b  14530  lssex  14663  cncrng  14878  psrbagfsupp  14978  psrbaglesupp  14981  eltpsg  15064  tg1  15083  cldval  15123  cldss  15129  cldopn  15131  psmetdmdm  15348  dvef  15751  relogef  15888  zabsle1  16032  usgredg2vlem2  16378  wlkprop  16482  wlkvtxiedg  16500  eupthseg  16607  bj-nn0suc0  16890