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	⊢ (𝜑 → 𝜓)
mpand.2	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mpand	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem mpand

Step	Hyp	Ref	Expression
1		mpand.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpand.2	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	ancomsd 269	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 432	1 ⊢ (𝜑 → (𝜒 → 𝜃))

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  7858  prcunqu  7859  p1le  9188  nnge1  9337  zltp1le  9711  gtndiv  9753  uzss  9960  addlelt  10187  xrre2  10241  xrre3  10242  zltaddlt1le  10428  nn0p1elfzo  10612  zsupcllemstep  10680  modfzo0difsn  10854  seqf1oglem1  10978  leexp2r  11052  expnlbnd2  11125  facavg  11207  wrdred1hash  11371  ccat2s1fvwd  11438  caubnd2  11907  maxleast  12003  mulcn2  12104  cn1lem  12106  climsqz  12127  climsqz2  12128  climcvg1nlem  12141  fsumabs  12258  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  bitsfzolem  12747  bitsfzo  12748  gcdzeq  12825  algcvgblem  12853  algcvga  12855  lcmdvdsb  12888  coprm  12949  pclemub  13096  bldisj  15639  xblm  15655  metss2lem  15735  bdxmet  15739  limccoap  15916  chtqub  16308  bcmono  16316  bclbnd  16319  bposlem1  16323  bposlem5  16327  bposlem6  16328  lgsne0  16374  gausslemma2dlem1a  16394  eupth2lemsfi  16936