Theorem syl2and 607

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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  anim12d  608  ax7  2020  dffi3  9120  cflim2  9950  axpre-sup  10856  xle2add  12922  fzen  13202  rpmulgcd2  16289  pcqmul  16482  initoeu1  17642  termoeu1  17649  plttr  17975  pospo  17978  lublecllem  17993  latjlej12  18088  latmlem12  18104  cygablOLD  19407  hausnei2  22412  uncmp  22462  itgsubst  25118  dvdsmulf1o  26248  2sqlem8a  26478  axcontlem9  27243  uspgr2wlkeq  27915  shintcli  29592  cvntr  30555  cdj3i  30704  f1resrcmplf1dlem  32958  satffunlem  33263  bj-bary1  35410  heicant  35739  itg2addnc  35758  dihmeetlem1N  39231  fmtnofac2lem  44908  2itscp  46015  mofsn  46059