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  7852  prcunqu  7853  p1le  9182  nnge1  9330  zltp1le  9704  gtndiv  9746  uzss  9953  addlelt  10180  xrre2  10234  xrre3  10235  zltaddlt1le  10421  nn0p1elfzo  10605  zsupcllemstep  10673  modfzo0difsn  10847  seqf1oglem1  10971  leexp2r  11045  expnlbnd2  11118  facavg  11200  wrdred1hash  11364  ccat2s1fvwd  11431  caubnd2  11900  maxleast  11996  mulcn2  12097  cn1lem  12099  climsqz  12120  climsqz2  12121  climcvg1nlem  12134  fsumabs  12251  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  bitsfzolem  12740  bitsfzo  12741  gcdzeq  12818  algcvgblem  12846  algcvga  12848  lcmdvdsb  12881  coprm  12942  pclemub  13089  bldisj  15593  xblm  15609  metss2lem  15689  bdxmet  15693  limccoap  15870  chtqub  16257  bcmono  16265  bclbnd  16268  bposlem1  16272  bposlem5  16276  bposlem6  16277  lgsne0  16323  gausslemma2dlem1a  16343  eupth2lemsfi  16885