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 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  609  ax7  2016  dffi3  9382  cflim2  10216  axpre-sup  11122  xle2add  13219  fzen  13502  rpmulgcd2  16626  pcqmul  16824  sbcie2s  17131  initoeu1  17973  termoeu1  17980  plttr  18301  pospo  18304  lublecllem  18319  latjlej12  18414  latmlem12  18430  hausnei2  23240  uncmp  23290  itgsubst  25956  mpodvdsmulf1o  27104  dvdsmulf1o  27106  2sqlem8a  27336  precsexlem10  28118  axcontlem9  28899  uspgr2wlkeq  29574  shintcli  31258  cvntr  32221  cdj3i  32370  f1resrcmplf1dlem  35076  satffunlem  35388  bj-bary1  37300  heicant  37649  itg2addnc  37668  dihmeetlem1N  41284  modelaxreplem1  44968  fmtnofac2lem  47569  2itscp  48770  mofsn  48832