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  2867  ovig  6041  prcdnql  7546  prcunqu  7547  p1le  8870  nnge1  9007  zltp1le  9374  gtndiv  9415  uzss  9616  addlelt  9837  xrre2  9890  xrre3  9891  zltaddlt1le  10076  modfzo0difsn  10469  seqf1oglem1  10593  leexp2r  10667  expnlbnd2  10739  facavg  10820  wrdred1hash  10960  caubnd2  11264  maxleast  11360  mulcn2  11458  cn1lem  11460  climsqz  11481  climsqz2  11482  climcvg1nlem  11495  fsumabs  11611  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  zsupcllemstep  12085  gcdzeq  12162  algcvgblem  12190  algcvga  12192  lcmdvdsb  12225  coprm  12285  pclemub  12428  bldisj  14580  xblm  14596  metss2lem  14676  bdxmet  14680  limccoap  14857  lgsne0  15195  gausslemma2dlem1a  15215