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  6213  prcdnql  7857  prcunqu  7858  p1le  9187  nnge1  9336  zltp1le  9708  gtndiv  9751  uzss  9958  addlelt  10185  xrre2  10239  xrre3  10240  zltaddlt1le  10426  nn0p1elfzo  10610  zsupcllemstep  10678  modfzo0difsn  10852  seqf1oglem1  10976  leexp2r  11050  expnlbnd2  11123  facavg  11205  wrdred1hash  11369  ccat2s1fvwd  11436  caubnd2  11905  maxleast  12001  mulcn2  12102  cn1lem  12104  climsqz  12125  climsqz2  12126  climcvg1nlem  12139  fsumabs  12256  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  bitsfzolem  12745  bitsfzo  12746  gcdzeq  12823  algcvgblem  12851  algcvga  12853  lcmdvdsb  12886  coprm  12947  pclemub  13094  bldisj  15644  xblm  15660  metss2lem  15740  bdxmet  15744  limccoap  15921  chtqub  16313  bcmono  16321  bclbnd  16324  bposlem1  16328  bposlem5  16332  bposlem6  16333  lgsne0  16379  gausslemma2dlem1a  16399  eupth2lemsfi  16941