Theorem syl2and 620

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)

Hypotheses

Ref	Expression
syl2and.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl2and.2	⊢ (𝜑 → (𝜃 → 𝜏))
syl2and.3	⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂))

Assertion

Ref	Expression
syl2and	⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Proof of Theorem syl2and

Step	Hyp	Ref	Expression
1		syl2and.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl2and.2	. . 3 ⊢ (𝜑 → (𝜃 → 𝜏))
3		syl2and.3	. . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂))
4	2, 3	sylan2d 617	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 615	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anim12d  621  ax7  2049  f1resrcmplf1dlem  7274  dffi3  9404  cflim2  10268  axpre-sup  11181  xle2add  13313  fzen  13597  rpmulgcd2  16750  pcqmul  16949  sbcie2s  17257  initoeu1  18104  termoeu1  18111  plttr  18432  pospo  18435  lublecllem  18450  latjlej12  18547  latmlem12  18563  hausnei2  23582  uncmp  23632  itgsubst  26281  mpodvdsmulf1o  27431  dvdsmulf1o  27433  2sqlem8a  27662  precsexlem10  28482  axcontlem9  29430  uspgr2wlkeq  30106  shintcli  31811  cvntr  32774  cdj3i  32923  satffunlem  35982  bj-bary1  38066  heicant  38406  itg2addnc  38425  findcard4  38465  dihmeetlem1N  42165  modelaxreplem1  45803  fmtnofac2lem  48473  2itscp  49713  mofsn  49774