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  6143  prcdnql  7704  prcunqu  7705  p1le  9029  nnge1  9166  zltp1le  9534  gtndiv  9575  uzss  9777  addlelt  10003  xrre2  10056  xrre3  10057  zltaddlt1le  10242  nn0p1elfzo  10422  zsupcllemstep  10490  modfzo0difsn  10658  seqf1oglem1  10782  leexp2r  10856  expnlbnd2  10928  facavg  11009  wrdred1hash  11161  ccat2s1fvwd  11228  caubnd2  11695  maxleast  11791  mulcn2  11890  cn1lem  11892  climsqz  11913  climsqz2  11914  climcvg1nlem  11927  fsumabs  12044  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  bitsfzolem  12533  bitsfzo  12534  gcdzeq  12611  algcvgblem  12639  algcvga  12641  lcmdvdsb  12674  coprm  12734  pclemub  12878  bldisj  15144  xblm  15160  metss2lem  15240  bdxmet  15244  limccoap  15421  lgsne0  15786  gausslemma2dlem1a  15806  eupth2lemsfi  16348