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  2880  ovig  6074  prcdnql  7604  prcunqu  7605  p1le  8929  nnge1  9066  zltp1le  9434  gtndiv  9475  uzss  9676  addlelt  9897  xrre2  9950  xrre3  9951  zltaddlt1le  10136  zsupcllemstep  10379  modfzo0difsn  10547  seqf1oglem1  10671  leexp2r  10745  expnlbnd2  10817  facavg  10898  wrdred1hash  11044  caubnd2  11472  maxleast  11568  mulcn2  11667  cn1lem  11669  climsqz  11690  climsqz2  11691  climcvg1nlem  11704  fsumabs  11820  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  bitsfzolem  12309  bitsfzo  12310  gcdzeq  12387  algcvgblem  12415  algcvga  12417  lcmdvdsb  12450  coprm  12510  pclemub  12654  bldisj  14917  xblm  14933  metss2lem  15013  bdxmet  15017  limccoap  15194  lgsne0  15559  gausslemma2dlem1a  15579