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

This theorem is referenced by:  anim12d  609  ax7  2019  dffi3  9422  cflim2  10254  axpre-sup  11160  xle2add  13234  fzen  13514  rpmulgcd2  16589  pcqmul  16782  sbcie2s  17090  initoeu1  17957  termoeu1  17964  plttr  18291  pospo  18294  lublecllem  18309  latjlej12  18404  latmlem12  18420  hausnei2  22848  uncmp  22898  itgsubst  25557  dvdsmulf1o  26687  2sqlem8a  26917  precsexlem10  27651  axcontlem9  28219  uspgr2wlkeq  28892  shintcli  30569  cvntr  31532  cdj3i  31681  f1resrcmplf1dlem  34077  satffunlem  34380  bj-bary1  36181  heicant  36511  itg2addnc  36530  dihmeetlem1N  40149  fmtnofac2lem  46222  2itscp  47420  mofsn  47463