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  2878  ovig  6057  prcdnql  7579  prcunqu  7580  p1le  8904  nnge1  9041  zltp1le  9409  gtndiv  9450  uzss  9651  addlelt  9872  xrre2  9925  xrre3  9926  zltaddlt1le  10111  zsupcllemstep  10353  modfzo0difsn  10521  seqf1oglem1  10645  leexp2r  10719  expnlbnd2  10791  facavg  10872  wrdred1hash  11012  caubnd2  11347  maxleast  11443  mulcn2  11542  cn1lem  11544  climsqz  11565  climsqz2  11566  climcvg1nlem  11579  fsumabs  11695  cvgratnnlemnexp  11754  cvgratnnlemmn  11755  bitsfzolem  12184  bitsfzo  12185  gcdzeq  12262  algcvgblem  12290  algcvga  12292  lcmdvdsb  12325  coprm  12385  pclemub  12529  bldisj  14791  xblm  14807  metss2lem  14887  bdxmet  14891  limccoap  15068  lgsne0  15433  gausslemma2dlem1a  15453