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  2925  ovig  6183  prcdnql  7815  prcunqu  7816  p1le  9140  nnge1  9277  zltp1le  9649  gtndiv  9691  uzss  9893  addlelt  10119  xrre2  10173  xrre3  10174  zltaddlt1le  10360  nn0p1elfzo  10543  zsupcllemstep  10611  modfzo0difsn  10781  seqf1oglem1  10905  leexp2r  10979  expnlbnd2  11052  facavg  11133  wrdred1hash  11293  ccat2s1fvwd  11360  caubnd2  11827  maxleast  11923  mulcn2  12022  cn1lem  12024  climsqz  12045  climsqz2  12046  climcvg1nlem  12059  fsumabs  12176  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  bitsfzolem  12665  bitsfzo  12666  gcdzeq  12743  algcvgblem  12771  algcvga  12773  lcmdvdsb  12806  coprm  12866  pclemub  13010  bldisj  15392  xblm  15408  metss2lem  15488  bdxmet  15492  limccoap  15669  lgsne0  16037  gausslemma2dlem1a  16057  eupth2lemsfi  16599