Theorem mpand 420

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 265	. 2 |- ( ph -> ( ( ch /\ ps ) -> th ) )
4	1, 3	mpan2d 419	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpani  421  mp2and  424  rspcimedv  2712  ovig  5673  prcdnql  6788  prcunqu  6789  p1le  8046  nnge1  8181  zltp1le  8538  gtndiv  8575  uzss  8772  addlelt  8972  xrre2  9016  xrre3  9017  zltaddlt1le  9156  modfzo0difsn  9529  leexp2r  9679  expnlbnd2  9747  facavg  9822  caubnd2  10204  maxleast  10300  mulcn2  10352  cn1lem  10353  climsqz  10374  climsqz2  10375  climcvg1nlem  10387  zsupcllemstep  10548  gcdzeq  10618  algcvgblem  10638  ialgcvga  10640  lcmdvdsb  10673  coprm  10730