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  5936  riotaprop  5997  unielxp  6337  dmtpos  6422  tpossym  6442  ercnv  6723  cnvct  6984  php5dom  7049  3xpfi  7126  recrecnq  7614  1idpr  7812  eqlei2  8274  lem1  9027  eluzfz1  10266  fzpred  10305  uznfz  10338  fz0fzdiffz0  10365  fzctr  10368  flid  10545  flqeqceilz  10581  faclbnd3  11006  bcn1  11021  isfinite4im  11055  leabs  11652  gcd0id  12568  lcmgcdlem  12667  dvdsnprmd  12715  pcprod  12937  fldivp1  12939  intopsn  13468  mgm1  13471  sgrp1  13512  mnd1  13556  mnd1id  13557  grp1  13707  grp1inv  13708  eqger  13829  eqgid  13831  qusghm  13887  rngressid  13986  ring1  14091  ringressid  14095  subrgsubm  14267  resrhm2b  14282  lssex  14387  cncrng  14602  eltpsg  14783  tg1  14802  cldval  14842  cldss  14848  cldopn  14850  psmetdmdm  15067  dvef  15470  relogef  15607  zabsle1  15747  usgredg2vlem2  16093  wlkprop  16197  wlkvtxiedg  16215  eupthseg  16322  bj-nn0suc0  16596