Theorem mpand 426

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpand.1	|- ( ph -> ps )
mpand.2	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
mpand	|- ( ph -> ( ch -> th ) )

Proof of Theorem mpand

Step	Hyp	Ref	Expression
1		mpand.1	. 2 |- ( ph -> ps )
2		mpand.2	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	ancomsd 267	. 2 |- ( ph -> ( ( ch /\ ps ) -> th ) )
4	1, 3	mpan2d 425	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpani  427  mp2and  430  rspcimedv  2832  ovig  5963  prcdnql  7425  prcunqu  7426  p1le  8744  nnge1  8880  zltp1le  9245  gtndiv  9286  uzss  9486  addlelt  9704  xrre2  9757  xrre3  9758  zltaddlt1le  9943  modfzo0difsn  10330  leexp2r  10509  expnlbnd2  10580  facavg  10659  caubnd2  11059  maxleast  11155  mulcn2  11253  cn1lem  11255  climsqz  11276  climsqz2  11277  climcvg1nlem  11290  fsumabs  11406  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  zsupcllemstep  11878  gcdzeq  11955  algcvgblem  11981  algcvga  11983  lcmdvdsb  12016  coprm  12076  pclemub  12219  bldisj  13041  xblm  13057  metss2lem  13137  bdxmet  13141  limccoap  13287  lgsne0  13579