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	⊢ (𝜑 → 𝜓)
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 428	1 ⊢ (𝜑 → (𝜒 → 𝜃))

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  2889  ovig  6097  prcdnql  7639  prcunqu  7640  p1le  8964  nnge1  9101  zltp1le  9469  gtndiv  9510  uzss  9711  addlelt  9932  xrre2  9985  xrre3  9986  zltaddlt1le  10171  zsupcllemstep  10416  modfzo0difsn  10584  seqf1oglem1  10708  leexp2r  10782  expnlbnd2  10854  facavg  10935  wrdred1hash  11081  caubnd2  11594  maxleast  11690  mulcn2  11789  cn1lem  11791  climsqz  11812  climsqz2  11813  climcvg1nlem  11826  fsumabs  11942  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  bitsfzolem  12431  bitsfzo  12432  gcdzeq  12509  algcvgblem  12537  algcvga  12539  lcmdvdsb  12572  coprm  12632  pclemub  12776  bldisj  15040  xblm  15056  metss2lem  15136  bdxmet  15140  limccoap  15317  lgsne0  15682  gausslemma2dlem1a  15702