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  2925  ovig  6183  prcdnql  7815  prcunqu  7816  p1le  9143  nnge1  9280  zltp1le  9652  gtndiv  9694  uzss  9896  addlelt  10122  xrre2  10176  xrre3  10177  zltaddlt1le  10363  nn0p1elfzo  10546  zsupcllemstep  10614  modfzo0difsn  10784  seqf1oglem1  10908  leexp2r  10982  expnlbnd2  11055  facavg  11136  wrdred1hash  11296  ccat2s1fvwd  11363  caubnd2  11830  maxleast  11926  mulcn2  12025  cn1lem  12027  climsqz  12048  climsqz2  12049  climcvg1nlem  12062  fsumabs  12179  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  bitsfzolem  12668  bitsfzo  12669  gcdzeq  12746  algcvgblem  12774  algcvga  12776  lcmdvdsb  12809  coprm  12869  pclemub  13013  bldisj  15395  xblm  15411  metss2lem  15491  bdxmet  15495  limccoap  15672  lgsne0  16040  gausslemma2dlem1a  16060  eupth2lemsfi  16602