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 207  df-an 396

This theorem is referenced by:  anim12d  608  ax7  2015  dffi3  9500  cflim2  10332  axpre-sup  11238  xle2add  13321  fzen  13601  rpmulgcd2  16703  pcqmul  16900  sbcie2s  17208  initoeu1  18078  termoeu1  18085  plttr  18412  pospo  18415  lublecllem  18430  latjlej12  18525  latmlem12  18541  hausnei2  23382  uncmp  23432  itgsubst  26110  mpodvdsmulf1o  27255  dvdsmulf1o  27257  2sqlem8a  27487  precsexlem10  28258  axcontlem9  29005  uspgr2wlkeq  29682  shintcli  31361  cvntr  32324  cdj3i  32473  f1resrcmplf1dlem  35062  satffunlem  35369  bj-bary1  37278  heicant  37615  itg2addnc  37634  dihmeetlem1N  41247  fmtnofac2lem  47442  2itscp  48515  mofsn  48557