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  3119  onsucelsucr  4612  sucunielr  4614  ordsuc  4667  peano2b  4719  xpiindim  4873  fununfun  5380  fvelrnb  5702  fliftcnv  5946  riotaprop  6007  unielxp  6346  dmtpos  6465  tpossym  6485  ercnv  6766  cnvct  7027  php5dom  7092  3xpfi  7169  recrecnq  7674  1idpr  7872  eqlei2  8333  lem1  9086  eluzfz1  10328  fzpred  10367  uznfz  10400  fz0fzdiffz0  10427  fzctr  10430  flid  10607  flqeqceilz  10643  faclbnd3  11068  bcn1  11083  isfinite4im  11117  leabs  11714  gcd0id  12630  lcmgcdlem  12729  dvdsnprmd  12777  pcprod  12999  fldivp1  13001  intopsn  13530  mgm1  13533  sgrp1  13574  mnd1  13618  mnd1id  13619  grp1  13769  grp1inv  13770  eqger  13891  eqgid  13893  qusghm  13949  rngressid  14048  ring1  14153  ringressid  14157  subrgsubm  14329  resrhm2b  14344  lssex  14450  cncrng  14665  psrbaglesupp  14769  eltpsg  14851  tg1  14870  cldval  14910  cldss  14916  cldopn  14918  psmetdmdm  15135  dvef  15538  relogef  15675  zabsle1  15818  usgredg2vlem2  16164  wlkprop  16268  wlkvtxiedg  16286  eupthseg  16393  bj-nn0suc0  16666