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  2911  ovig  6148  prcdnql  7709  prcunqu  7710  p1le  9034  nnge1  9171  zltp1le  9539  gtndiv  9580  uzss  9782  addlelt  10008  xrre2  10061  xrre3  10062  zltaddlt1le  10247  nn0p1elfzo  10427  zsupcllemstep  10495  modfzo0difsn  10663  seqf1oglem1  10787  leexp2r  10861  expnlbnd2  10933  facavg  11014  wrdred1hash  11166  ccat2s1fvwd  11233  caubnd2  11700  maxleast  11796  mulcn2  11895  cn1lem  11897  climsqz  11918  climsqz2  11919  climcvg1nlem  11932  fsumabs  12049  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  bitsfzolem  12538  bitsfzo  12539  gcdzeq  12616  algcvgblem  12644  algcvga  12646  lcmdvdsb  12679  coprm  12739  pclemub  12883  bldisj  15154  xblm  15170  metss2lem  15250  bdxmet  15254  limccoap  15431  lgsne0  15796  gausslemma2dlem1a  15816  eupth2lemsfi  16358