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  2925  ovig  6184  prcdnql  7816  prcunqu  7817  p1le  9144  nnge1  9281  zltp1le  9653  gtndiv  9695  uzss  9897  addlelt  10123  xrre2  10177  xrre3  10178  zltaddlt1le  10364  nn0p1elfzo  10547  zsupcllemstep  10615  modfzo0difsn  10785  seqf1oglem1  10909  leexp2r  10983  expnlbnd2  11056  facavg  11137  wrdred1hash  11297  ccat2s1fvwd  11364  caubnd2  11832  maxleast  11928  mulcn2  12027  cn1lem  12029  climsqz  12050  climsqz2  12051  climcvg1nlem  12064  fsumabs  12181  cvgratnnlemnexp  12240  cvgratnnlemmn  12241  bitsfzolem  12670  bitsfzo  12671  gcdzeq  12748  algcvgblem  12776  algcvga  12778  lcmdvdsb  12811  coprm  12871  pclemub  13015  bldisj  15397  xblm  15413  metss2lem  15493  bdxmet  15497  limccoap  15674  lgsne0  16042  gausslemma2dlem1a  16062  eupth2lemsfi  16604