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  2843  ovig  5995  prcdnql  7482  prcunqu  7483  p1le  8804  nnge1  8940  zltp1le  9305  gtndiv  9346  uzss  9546  addlelt  9766  xrre2  9819  xrre3  9820  zltaddlt1le  10005  modfzo0difsn  10392  leexp2r  10571  expnlbnd2  10642  facavg  10721  caubnd2  11121  maxleast  11217  mulcn2  11315  cn1lem  11317  climsqz  11338  climsqz2  11339  climcvg1nlem  11352  fsumabs  11468  cvgratnnlemnexp  11527  cvgratnnlemmn  11528  zsupcllemstep  11940  gcdzeq  12017  algcvgblem  12043  algcvga  12045  lcmdvdsb  12078  coprm  12138  pclemub  12281  bldisj  13794  xblm  13810  metss2lem  13890  bdxmet  13894  limccoap  14040  lgsne0  14332