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  3115  onsucelsucr  4600  sucunielr  4602  ordsuc  4655  peano2b  4707  xpiindim  4859  fununfun  5364  fvelrnb  5681  fliftcnv  5919  riotaprop  5980  unielxp  6320  dmtpos  6402  tpossym  6422  ercnv  6701  cnvct  6962  php5dom  7024  3xpfi  7095  recrecnq  7581  1idpr  7779  eqlei2  8241  lem1  8994  eluzfz1  10227  fzpred  10266  uznfz  10299  fz0fzdiffz0  10326  fzctr  10329  flid  10504  flqeqceilz  10540  faclbnd3  10965  bcn1  10980  isfinite4im  11014  leabs  11585  gcd0id  12500  lcmgcdlem  12599  dvdsnprmd  12647  pcprod  12869  fldivp1  12871  intopsn  13400  mgm1  13403  sgrp1  13444  mnd1  13488  mnd1id  13489  grp1  13639  grp1inv  13640  eqger  13761  eqgid  13763  qusghm  13819  rngressid  13917  ring1  14022  ringressid  14026  subrgsubm  14198  resrhm2b  14213  lssex  14318  cncrng  14533  eltpsg  14714  tg1  14733  cldval  14773  cldss  14779  cldopn  14781  psmetdmdm  14998  dvef  15401  relogef  15538  zabsle1  15678  usgredg2vlem2  16021  wlkprop  16039  wlkvtxiedg  16056  bj-nn0suc0  16313