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 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  610  ax7  2018  dffi3  9346  cflim2  10185  axpre-sup  11092  xle2add  13186  fzen  13469  rpmulgcd2  16595  pcqmul  16793  sbcie2s  17100  initoeu1  17947  termoeu1  17954  plttr  18275  pospo  18278  lublecllem  18293  latjlej12  18390  latmlem12  18406  hausnei2  23309  uncmp  23359  itgsubst  26024  mpodvdsmulf1o  27172  dvdsmulf1o  27174  2sqlem8a  27404  precsexlem10  28224  axcontlem9  29057  uspgr2wlkeq  29731  shintcli  31416  cvntr  32379  cdj3i  32528  f1resrcmplf1dlem  35261  satffunlem  35614  bj-bary1  37556  heicant  37895  itg2addnc  37914  dihmeetlem1N  41655  modelaxreplem1  45323  fmtnofac2lem  47917  2itscp  49130  mofsn  49192