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  3116  onsucelsucr  4604  sucunielr  4606  ordsuc  4659  peano2b  4711  xpiindim  4865  fununfun  5370  fvelrnb  5689  fliftcnv  5931  riotaprop  5992  unielxp  6332  dmtpos  6417  tpossym  6437  ercnv  6718  cnvct  6979  php5dom  7044  3xpfi  7118  recrecnq  7604  1idpr  7802  eqlei2  8264  lem1  9017  eluzfz1  10256  fzpred  10295  uznfz  10328  fz0fzdiffz0  10355  fzctr  10358  flid  10534  flqeqceilz  10570  faclbnd3  10995  bcn1  11010  isfinite4im  11044  leabs  11625  gcd0id  12540  lcmgcdlem  12639  dvdsnprmd  12687  pcprod  12909  fldivp1  12911  intopsn  13440  mgm1  13443  sgrp1  13484  mnd1  13528  mnd1id  13529  grp1  13679  grp1inv  13680  eqger  13801  eqgid  13803  qusghm  13859  rngressid  13957  ring1  14062  ringressid  14066  subrgsubm  14238  resrhm2b  14253  lssex  14358  cncrng  14573  eltpsg  14754  tg1  14773  cldval  14813  cldss  14819  cldopn  14821  psmetdmdm  15038  dvef  15441  relogef  15578  zabsle1  15718  usgredg2vlem2  16062  wlkprop  16124  wlkvtxiedg  16142  eupthseg  16247  bj-nn0suc0  16481