Theorem mpand 433

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 432	1 |- ( ph -> ( ch -> th ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpani  434  mp2and  437  rspcimedv  2931  ovig  6210  prcdnql  7851  prcunqu  7852  p1le  9181  nnge1  9329  zltp1le  9703  gtndiv  9745  uzss  9952  addlelt  10179  xrre2  10233  xrre3  10234  zltaddlt1le  10420  nn0p1elfzo  10604  zsupcllemstep  10672  modfzo0difsn  10845  seqf1oglem1  10969  leexp2r  11043  expnlbnd2  11116  facavg  11198  wrdred1hash  11362  ccat2s1fvwd  11429  caubnd2  11898  maxleast  11994  mulcn2  12094  cn1lem  12096  climsqz  12117  climsqz2  12118  climcvg1nlem  12131  fsumabs  12248  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  bitsfzolem  12737  bitsfzo  12738  gcdzeq  12815  algcvgblem  12843  algcvga  12845  lcmdvdsb  12878  coprm  12939  pclemub  13086  bldisj  15551  xblm  15567  metss2lem  15647  bdxmet  15651  limccoap  15828  bcmono  16202  bclbnd  16205  bposlem1  16209  bposlem5  16213  lgsne0  16255  gausslemma2dlem1a  16275  eupth2lemsfi  16817