Theorem syl2and 614

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anim12d  615  ax7  2023  dffi3  9341  cflim2  10183  axpre-sup  11090  xle2add  13209  fzen  13493  rpmulgcd2  16623  pcqmul  16822  sbcie2s  17129  initoeu1  17976  termoeu1  17983  plttr  18304  pospo  18307  lublecllem  18322  latjlej12  18419  latmlem12  18435  hausnei2  23343  uncmp  23393  itgsubst  26041  mpodvdsmulf1o  27182  dvdsmulf1o  27184  2sqlem8a  27413  precsexlem10  28233  axcontlem9  29066  uspgr2wlkeq  29739  shintcli  31425  cvntr  32388  cdj3i  32537  f1resrcmplf1dlem  35276  satffunlem  35630  bj-bary1  37673  heicant  38023  itg2addnc  38042  dihmeetlem1N  41783  modelaxreplem1  45423  fmtnofac2lem  48047  2itscp  49273  mofsn  49335