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  3129  onsucelsucr  4630  sucunielr  4632  ordsuc  4685  peano2b  4737  xpiindim  4892  fununfun  5399  fvelrnb  5724  fliftcnv  5968  riotaprop  6029  unielxp  6368  dmtpos  6487  tpossym  6507  ercnv  6788  cnvct  7050  php5dom  7117  3xpfi  7194  recrecnq  7709  1idpr  7907  eqlei2  8368  lem1  9121  eluzfz1  10365  fzpred  10404  uznfz  10437  fz0fzdiffz0  10464  fzctr  10467  flid  10644  flqeqceilz  10680  faclbnd3  11105  bcn1  11120  isfinite4im  11155  leabs  11759  gcd0id  12675  lcmgcdlem  12774  dvdsnprmd  12822  pcprod  13044  fldivp1  13046  intopsn  13580  mgm1  13583  sgrp1  13624  mnd1  13668  mnd1id  13669  grp1  13819  grp1inv  13820  eqger  13941  eqgid  13943  qusghm  13999  rngressid  14098  ring1  14203  ringressid  14207  subrgsubm  14379  resrhm2b  14394  lssex  14502  cncrng  14717  psrbagfsupp  14819  psrbaglesupp  14822  eltpsg  14905  tg1  14924  cldval  14964  cldss  14970  cldopn  14972  psmetdmdm  15189  dvef  15592  relogef  15729  zabsle1  15872  usgredg2vlem2  16218  wlkprop  16322  wlkvtxiedg  16340  eupthseg  16447  bj-nn0suc0  16720