Theorem mpand 419

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 265	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 418	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpani  420  mp2and  423  rspcimedv  2703  ovig  5642  prcdnql  6674  prcunqu  6675  p1le  7927  nnge1  8062  zltp1le  8405  gtndiv  8442  uzss  8639  addlelt  8839  xrre2  8888  xrre3  8889  zltaddlt1le  9028  modfzo0difsn  9397  leexp2r  9530  expnlbnd2  9598  facavg  9673  caubnd2  10003  maxleast  10099  mulcn2  10151  cn1lem  10152  climsqz  10173  climsqz2  10174  climcvg1nlem  10186  zsupcllemstep  10341  gcdzeq  10411  algcvgblem  10431  ialgcvga  10433  lcmdvdsb  10466  coprm  10523