Theorem mpand 425

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpani  426  mp2and  429  rspcimedv  2786  ovig  5885  prcdnql  7285  prcunqu  7286  p1le  8600  nnge1  8736  zltp1le  9101  gtndiv  9139  uzss  9339  addlelt  9548  xrre2  9597  xrre3  9598  zltaddlt1le  9782  modfzo0difsn  10161  leexp2r  10340  expnlbnd2  10410  facavg  10485  caubnd2  10882  maxleast  10978  mulcn2  11074  cn1lem  11076  climsqz  11097  climsqz2  11098  climcvg1nlem  11111  fsumabs  11227  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  zsupcllemstep  11627  gcdzeq  11699  algcvgblem  11719  algcvga  11721  lcmdvdsb  11754  coprm  11811  bldisj  12559  xblm  12575  metss2lem  12655  bdxmet  12659  limccoap  12805