Theorem syl2and 608

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 605	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 603	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 207  df-an 396

This theorem is referenced by:  anim12d  609  ax7  2015  dffi3  9471  cflim2  10303  axpre-sup  11209  xle2add  13301  fzen  13581  rpmulgcd2  16693  pcqmul  16891  sbcie2s  17198  initoeu1  18056  termoeu1  18063  plttr  18387  pospo  18390  lublecllem  18405  latjlej12  18500  latmlem12  18516  hausnei2  23361  uncmp  23411  itgsubst  26090  mpodvdsmulf1o  27237  dvdsmulf1o  27239  2sqlem8a  27469  precsexlem10  28240  axcontlem9  28987  uspgr2wlkeq  29664  shintcli  31348  cvntr  32311  cdj3i  32460  f1resrcmplf1dlem  35100  satffunlem  35406  bj-bary1  37313  heicant  37662  itg2addnc  37681  dihmeetlem1N  41292  modelaxreplem1  44995  fmtnofac2lem  47555  2itscp  48702  mofsn  48753