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  9179  nnge1  9327  zltp1le  9699  gtndiv  9741  uzss  9943  addlelt  10169  xrre2  10223  xrre3  10224  zltaddlt1le  10410  nn0p1elfzo  10594  zsupcllemstep  10662  modfzo0difsn  10832  seqf1oglem1  10956  leexp2r  11030  expnlbnd2  11103  facavg  11184  wrdred1hash  11348  ccat2s1fvwd  11415  caubnd2  11883  maxleast  11979  mulcn2  12078  cn1lem  12080  climsqz  12101  climsqz2  12102  climcvg1nlem  12115  fsumabs  12232  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  bitsfzolem  12721  bitsfzo  12722  gcdzeq  12799  algcvgblem  12827  algcvga  12829  lcmdvdsb  12862  coprm  12922  pclemub  13066  bldisj  15502  xblm  15518  metss2lem  15598  bdxmet  15602  limccoap  15779  lgsne0  16157  gausslemma2dlem1a  16177  eupth2lemsfi  16719