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  2883  ovig  6080  prcdnql  7617  prcunqu  7618  p1le  8942  nnge1  9079  zltp1le  9447  gtndiv  9488  uzss  9689  addlelt  9910  xrre2  9963  xrre3  9964  zltaddlt1le  10149  zsupcllemstep  10394  modfzo0difsn  10562  seqf1oglem1  10686  leexp2r  10760  expnlbnd2  10832  facavg  10913  wrdred1hash  11059  caubnd2  11503  maxleast  11599  mulcn2  11698  cn1lem  11700  climsqz  11721  climsqz2  11722  climcvg1nlem  11735  fsumabs  11851  cvgratnnlemnexp  11910  cvgratnnlemmn  11911  bitsfzolem  12340  bitsfzo  12341  gcdzeq  12418  algcvgblem  12446  algcvga  12448  lcmdvdsb  12481  coprm  12541  pclemub  12685  bldisj  14948  xblm  14964  metss2lem  15044  bdxmet  15048  limccoap  15225  lgsne0  15590  gausslemma2dlem1a  15610