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  3118  onsucelsucr  4606  sucunielr  4608  ordsuc  4661  peano2b  4713  xpiindim  4867  fununfun  5373  fvelrnb  5693  fliftcnv  5935  riotaprop  5996  unielxp  6336  dmtpos  6421  tpossym  6441  ercnv  6722  cnvct  6983  php5dom  7048  3xpfi  7125  recrecnq  7613  1idpr  7811  eqlei2  8273  lem1  9026  eluzfz1  10265  fzpred  10304  uznfz  10337  fz0fzdiffz0  10364  fzctr  10367  flid  10543  flqeqceilz  10579  faclbnd3  11004  bcn1  11019  isfinite4im  11053  leabs  11634  gcd0id  12549  lcmgcdlem  12648  dvdsnprmd  12696  pcprod  12918  fldivp1  12920  intopsn  13449  mgm1  13452  sgrp1  13493  mnd1  13537  mnd1id  13538  grp1  13688  grp1inv  13689  eqger  13810  eqgid  13812  qusghm  13868  rngressid  13966  ring1  14071  ringressid  14075  subrgsubm  14247  resrhm2b  14262  lssex  14367  cncrng  14582  eltpsg  14763  tg1  14782  cldval  14822  cldss  14828  cldopn  14830  psmetdmdm  15047  dvef  15450  relogef  15587  zabsle1  15727  usgredg2vlem2  16073  wlkprop  16177  wlkvtxiedg  16195  eupthseg  16302  bj-nn0suc0  16545