Theorem mpand 423

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 267	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 422	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpani  424  mp2and  427  rspcimedv  2762  ovig  5846  prcdnql  7237  prcunqu  7238  p1le  8514  nnge1  8650  zltp1le  9009  gtndiv  9047  uzss  9245  addlelt  9445  xrre2  9494  xrre3  9495  zltaddlt1le  9679  modfzo0difsn  10058  leexp2r  10237  expnlbnd2  10307  facavg  10382  caubnd2  10778  maxleast  10874  mulcn2  10970  cn1lem  10972  climsqz  10993  climsqz2  10994  climcvg1nlem  11007  fsumabs  11123  cvgratnnlemnexp  11182  cvgratnnlemmn  11183  zsupcllemstep  11483  gcdzeq  11553  algcvgblem  11573  algcvga  11575  lcmdvdsb  11608  coprm  11665  bldisj  12387  xblm  12403  metss2lem  12483  bdxmet  12487