Theorem mpand 427

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 426	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  428  mp2and  431  rspcimedv  2836  ovig  5974  prcdnql  7446  prcunqu  7447  p1le  8765  nnge1  8901  zltp1le  9266  gtndiv  9307  uzss  9507  addlelt  9725  xrre2  9778  xrre3  9779  zltaddlt1le  9964  modfzo0difsn  10351  leexp2r  10530  expnlbnd2  10601  facavg  10680  caubnd2  11081  maxleast  11177  mulcn2  11275  cn1lem  11277  climsqz  11298  climsqz2  11299  climcvg1nlem  11312  fsumabs  11428  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  zsupcllemstep  11900  gcdzeq  11977  algcvgblem  12003  algcvga  12005  lcmdvdsb  12038  coprm  12098  pclemub  12241  bldisj  13195  xblm  13211  metss2lem  13291  bdxmet  13295  limccoap  13441  lgsne0  13733