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  2870  ovig  6048  prcdnql  7568  prcunqu  7569  p1le  8893  nnge1  9030  zltp1le  9397  gtndiv  9438  uzss  9639  addlelt  9860  xrre2  9913  xrre3  9914  zltaddlt1le  10099  zsupcllemstep  10336  modfzo0difsn  10504  seqf1oglem1  10628  leexp2r  10702  expnlbnd2  10774  facavg  10855  wrdred1hash  10995  caubnd2  11299  maxleast  11395  mulcn2  11494  cn1lem  11496  climsqz  11517  climsqz2  11518  climcvg1nlem  11531  fsumabs  11647  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  bitsfzolem  12136  bitsfzo  12137  gcdzeq  12214  algcvgblem  12242  algcvga  12244  lcmdvdsb  12277  coprm  12337  pclemub  12481  bldisj  14721  xblm  14737  metss2lem  14817  bdxmet  14821  limccoap  14998  lgsne0  15363  gausslemma2dlem1a  15383