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  2912  ovig  6142  prcdnql  7703  prcunqu  7704  p1le  9028  nnge1  9165  zltp1le  9533  gtndiv  9574  uzss  9776  addlelt  10002  xrre2  10055  xrre3  10056  zltaddlt1le  10241  zsupcllemstep  10488  modfzo0difsn  10656  seqf1oglem1  10780  leexp2r  10854  expnlbnd2  10926  facavg  11007  wrdred1hash  11156  ccat2s1fvwd  11223  caubnd2  11677  maxleast  11773  mulcn2  11872  cn1lem  11874  climsqz  11895  climsqz2  11896  climcvg1nlem  11909  fsumabs  12025  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  bitsfzolem  12514  bitsfzo  12515  gcdzeq  12592  algcvgblem  12620  algcvga  12622  lcmdvdsb  12655  coprm  12715  pclemub  12859  bldisj  15124  xblm  15140  metss2lem  15220  bdxmet  15224  limccoap  15401  lgsne0  15766  gausslemma2dlem1a  15786