Theorem syl2and 609

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  anim12d  610  ax7  2019  dffi3  9292  cflim2  10124  axpre-sup  11030  xle2add  13098  fzen  13378  rpmulgcd2  16458  pcqmul  16651  initoeu1  17823  termoeu1  17830  plttr  18157  pospo  18160  lublecllem  18175  latjlej12  18270  latmlem12  18286  hausnei2  22609  uncmp  22659  itgsubst  25318  dvdsmulf1o  26448  2sqlem8a  26678  axcontlem9  27628  uspgr2wlkeq  28301  shintcli  29978  cvntr  30941  cdj3i  31090  f1resrcmplf1dlem  33355  satffunlem  33660  bj-bary1  35637  heicant  35968  itg2addnc  35987  dihmeetlem1N  39609  fmtnofac2lem  45438  2itscp  46545  mofsn  46589