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  2909  ovig  6132  prcdnql  7682  prcunqu  7683  p1le  9007  nnge1  9144  zltp1le  9512  gtndiv  9553  uzss  9755  addlelt  9976  xrre2  10029  xrre3  10030  zltaddlt1le  10215  zsupcllemstep  10461  modfzo0difsn  10629  seqf1oglem1  10753  leexp2r  10827  expnlbnd2  10899  facavg  10980  wrdred1hash  11128  caubnd2  11643  maxleast  11739  mulcn2  11838  cn1lem  11840  climsqz  11861  climsqz2  11862  climcvg1nlem  11875  fsumabs  11991  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  bitsfzolem  12480  bitsfzo  12481  gcdzeq  12558  algcvgblem  12586  algcvga  12588  lcmdvdsb  12621  coprm  12681  pclemub  12825  bldisj  15090  xblm  15106  metss2lem  15186  bdxmet  15190  limccoap  15367  lgsne0  15732  gausslemma2dlem1a  15752