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  2912  ovig  6143  prcdnql  7704  prcunqu  7705  p1le  9029  nnge1  9166  zltp1le  9534  gtndiv  9575  uzss  9777  addlelt  10003  xrre2  10056  xrre3  10057  zltaddlt1le  10242  nn0p1elfzo  10422  zsupcllemstep  10490  modfzo0difsn  10658  seqf1oglem1  10782  leexp2r  10856  expnlbnd2  10928  facavg  11009  wrdred1hash  11158  ccat2s1fvwd  11225  caubnd2  11679  maxleast  11775  mulcn2  11874  cn1lem  11876  climsqz  11897  climsqz2  11898  climcvg1nlem  11911  fsumabs  12028  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  bitsfzolem  12517  bitsfzo  12518  gcdzeq  12595  algcvgblem  12623  algcvga  12625  lcmdvdsb  12658  coprm  12718  pclemub  12862  bldisj  15128  xblm  15144  metss2lem  15224  bdxmet  15228  limccoap  15405  lgsne0  15770  gausslemma2dlem1a  15790  eupth2lemsfi  16332