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 398

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 209  df-an 399

This theorem is referenced by:  anim12d  610  ax7  2023  dffi3  8895  cflim2  9685  axpre-sup  10591  xle2add  12653  fzen  12925  rpmulgcd2  16000  pcqmul  16190  initoeu1  17271  termoeu1  17278  plttr  17580  pospo  17583  lublecllem  17598  latjlej12  17677  latmlem12  17693  cygablOLD  19011  hausnei2  21961  uncmp  22011  itgsubst  24646  dvdsmulf1o  25771  2sqlem8a  26001  axcontlem9  26758  uspgr2wlkeq  27427  shintcli  29106  cvntr  30069  cdj3i  30218  f1resrcmplf1dlem  32359  satffunlem  32648  bj-bary1  34596  heicant  34942  itg2addnc  34961  dihmeetlem1N  38441  fmtnofac2lem  43750  2itscp  44788