Theorem mpand 429

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpani  430  mp2and  433  rspcimedv  2870  ovig  6044  prcdnql  7551  prcunqu  7552  p1le  8876  nnge1  9013  zltp1le  9380  gtndiv  9421  uzss  9622  addlelt  9843  xrre2  9896  xrre3  9897  zltaddlt1le  10082  zsupcllemstep  10319  modfzo0difsn  10487  seqf1oglem1  10611  leexp2r  10685  expnlbnd2  10757  facavg  10838  wrdred1hash  10978  caubnd2  11282  maxleast  11378  mulcn2  11477  cn1lem  11479  climsqz  11500  climsqz2  11501  climcvg1nlem  11514  fsumabs  11630  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  bitsfzolem  12118  bitsfzo  12119  gcdzeq  12189  algcvgblem  12217  algcvga  12219  lcmdvdsb  12252  coprm  12312  pclemub  12456  bldisj  14637  xblm  14653  metss2lem  14733  bdxmet  14737  limccoap  14914  lgsne0  15279  gausslemma2dlem1a  15299