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  2913  ovig  6153  prcdnql  7747  prcunqu  7748  p1le  9071  nnge1  9208  zltp1le  9578  gtndiv  9619  uzss  9821  addlelt  10047  xrre2  10100  xrre3  10101  zltaddlt1le  10287  nn0p1elfzo  10467  zsupcllemstep  10535  modfzo0difsn  10703  seqf1oglem1  10827  leexp2r  10901  expnlbnd2  10973  facavg  11054  wrdred1hash  11206  ccat2s1fvwd  11273  caubnd2  11740  maxleast  11836  mulcn2  11935  cn1lem  11937  climsqz  11958  climsqz2  11959  climcvg1nlem  11972  fsumabs  12089  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  bitsfzolem  12578  bitsfzo  12579  gcdzeq  12656  algcvgblem  12684  algcvga  12686  lcmdvdsb  12719  coprm  12779  pclemub  12923  bldisj  15195  xblm  15211  metss2lem  15291  bdxmet  15295  limccoap  15472  lgsne0  15840  gausslemma2dlem1a  15860  eupth2lemsfi  16402