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  3132  onsucelsucr  4635  sucunielr  4637  ordsuc  4690  peano2b  4742  xpiindim  4897  fununfun  5404  fvelrnb  5729  fliftcnv  5974  riotaprop  6037  unielxp  6381  dmtpos  6500  tpossym  6520  ercnv  6801  cnvct  7063  php5dom  7130  3xpfi  7207  recrecnq  7725  1idpr  7923  eqlei2  8384  lem1  9138  eluzfz1  10385  fzpred  10426  uznfz  10459  fz0fzdiffz0  10486  fzctr  10489  flid  10668  flqeqceilz  10704  faclbnd3  11130  bcn1  11145  isfinite4im  11180  leabs  11784  gcd0id  12700  lcmgcdlem  12799  dvdsnprmd  12847  pcprod  13069  fldivp1  13071  intopsn  13630  mgm1  13633  sgrp1  13674  mnd1  13710  mnd1id  13711  grp1  13861  grp1inv  13862  eqger  13977  eqgid  13979  qusghm  14035  rngressid  14193  ring1  14302  ringressid  14306  subrgsubm  14480  resrhm2b  14495  lssex  14628  cncrng  14843  psrbagfsupp  14945  psrbaglesupp  14948  eltpsg  15031  tg1  15050  cldval  15090  cldss  15096  cldopn  15098  psmetdmdm  15315  dvef  15718  relogef  15855  zabsle1  15998  usgredg2vlem2  16344  wlkprop  16448  wlkvtxiedg  16466  eupthseg  16573  bj-nn0suc0  16846