Theorem syl2and 606

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 603	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 601	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))

Syntax hints:   → wi 4   ∧ wa 394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  anim12d  607  ax7  2017  dffi3  9428  cflim2  10260  axpre-sup  11166  xle2add  13242  fzen  13522  rpmulgcd2  16597  pcqmul  16790  sbcie2s  17098  initoeu1  17965  termoeu1  17972  plttr  18299  pospo  18302  lublecllem  18317  latjlej12  18412  latmlem12  18428  hausnei2  23077  uncmp  23127  itgsubst  25801  dvdsmulf1o  26934  2sqlem8a  27164  precsexlem10  27901  axcontlem9  28497  uspgr2wlkeq  29170  shintcli  30849  cvntr  31812  cdj3i  31961  f1resrcmplf1dlem  34387  satffunlem  34690  bj-bary1  36496  heicant  36826  itg2addnc  36845  dihmeetlem1N  40464  fmtnofac2lem  46534  2itscp  47554  mofsn  47597