Theorem mpand 433

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 432	1 |- ( ph -> ( ch -> th ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpani  434  mp2and  437  rspcimedv  2931  ovig  6213  prcdnql  7857  prcunqu  7858  p1le  9187  nnge1  9336  zltp1le  9710  gtndiv  9752  uzss  9959  addlelt  10186  xrre2  10240  xrre3  10241  zltaddlt1le  10427  nn0p1elfzo  10611  zsupcllemstep  10679  modfzo0difsn  10853  seqf1oglem1  10977  leexp2r  11051  expnlbnd2  11124  facavg  11206  wrdred1hash  11370  ccat2s1fvwd  11437  caubnd2  11906  maxleast  12002  mulcn2  12103  cn1lem  12105  climsqz  12126  climsqz2  12127  climcvg1nlem  12140  fsumabs  12257  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  bitsfzolem  12746  bitsfzo  12747  gcdzeq  12824  algcvgblem  12852  algcvga  12854  lcmdvdsb  12887  coprm  12948  pclemub  13095  bldisj  15627  xblm  15643  metss2lem  15723  bdxmet  15727  limccoap  15904  chtqub  16296  bcmono  16304  bclbnd  16307  bposlem1  16311  bposlem5  16315  bposlem6  16316  lgsne0  16362  gausslemma2dlem1a  16382  eupth2lemsfi  16924