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  2909  ovig  6135  prcdnql  7687  prcunqu  7688  p1le  9012  nnge1  9149  zltp1le  9517  gtndiv  9558  uzss  9760  addlelt  9981  xrre2  10034  xrre3  10035  zltaddlt1le  10220  zsupcllemstep  10466  modfzo0difsn  10634  seqf1oglem1  10758  leexp2r  10832  expnlbnd2  10904  facavg  10985  wrdred1hash  11133  caubnd2  11649  maxleast  11745  mulcn2  11844  cn1lem  11846  climsqz  11867  climsqz2  11868  climcvg1nlem  11881  fsumabs  11997  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  bitsfzolem  12486  bitsfzo  12487  gcdzeq  12564  algcvgblem  12592  algcvga  12594  lcmdvdsb  12627  coprm  12687  pclemub  12831  bldisj  15096  xblm  15112  metss2lem  15192  bdxmet  15196  limccoap  15373  lgsne0  15738  gausslemma2dlem1a  15758