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  2844  ovig  5996  prcdnql  7483  prcunqu  7484  p1le  8806  nnge1  8942  zltp1le  9307  gtndiv  9348  uzss  9548  addlelt  9768  xrre2  9821  xrre3  9822  zltaddlt1le  10007  modfzo0difsn  10395  leexp2r  10574  expnlbnd2  10646  facavg  10726  caubnd2  11126  maxleast  11222  mulcn2  11320  cn1lem  11322  climsqz  11343  climsqz2  11344  climcvg1nlem  11357  fsumabs  11473  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  zsupcllemstep  11946  gcdzeq  12023  algcvgblem  12049  algcvga  12051  lcmdvdsb  12084  coprm  12144  pclemub  12287  bldisj  13904  xblm  13920  metss2lem  14000  bdxmet  14004  limccoap  14150  lgsne0  14442