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  2795  ovig  5900  prcdnql  7316  prcunqu  7317  p1le  8631  nnge1  8767  zltp1le  9132  gtndiv  9170  uzss  9370  addlelt  9585  xrre2  9634  xrre3  9635  zltaddlt1le  9820  modfzo0difsn  10199  leexp2r  10378  expnlbnd2  10448  facavg  10524  caubnd2  10921  maxleast  11017  mulcn2  11113  cn1lem  11115  climsqz  11136  climsqz2  11137  climcvg1nlem  11150  fsumabs  11266  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  zsupcllemstep  11674  gcdzeq  11746  algcvgblem  11766  algcvga  11768  lcmdvdsb  11801  coprm  11858  bldisj  12609  xblm  12625  metss2lem  12705  bdxmet  12709  limccoap  12855