Theorem mpand 433

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 432	1 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpani  434  mp2and  437  rspcimedv  2931  ovig  6210  prcdnql  7851  prcunqu  7852  p1le  9180  nnge1  9328  zltp1le  9701  gtndiv  9743  uzss  9945  addlelt  10171  xrre2  10225  xrre3  10226  zltaddlt1le  10412  nn0p1elfzo  10596  zsupcllemstep  10664  modfzo0difsn  10834  seqf1oglem1  10958  leexp2r  11032  expnlbnd2  11105  facavg  11186  wrdred1hash  11350  ccat2s1fvwd  11417  caubnd2  11885  maxleast  11981  mulcn2  12080  cn1lem  12082  climsqz  12103  climsqz2  12104  climcvg1nlem  12117  fsumabs  12234  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  bitsfzolem  12723  bitsfzo  12724  gcdzeq  12801  algcvgblem  12829  algcvga  12831  lcmdvdsb  12864  coprm  12924  pclemub  13068  bldisj  15504  xblm  15520  metss2lem  15600  bdxmet  15604  limccoap  15781  bcmono  16124  bclbnd  16127  lgsne0  16169  gausslemma2dlem1a  16189  eupth2lemsfi  16731