Theorem syl2and 620

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anim12d  621  ax7  2051  f1resrcmplf1dlem  7301  dffi3  9450  cflim2  10368  axpre-sup  11281  xle2add  13416  fzen  13701  rpmulgcd2  16860  pcqmul  17060  sbcie2s  17368  initoeu1  18215  termoeu1  18222  plttr  18543  pospo  18546  lublecllem  18561  latjlej12  18658  latmlem12  18674  hausnei2  23701  uncmp  23751  itgsubst  26399  mpodvdsmulf1o  27551  dvdsmulf1o  27553  2sqlem8a  27782  precsexlem10  28632  axcontlem9  29580  uspgr2wlkeq  30256  shintcli  31961  cvntr  32924  cdj3i  33073  satffunlem  36333  bj-bary1  38425  heicant  38765  itg2addnc  38784  findcard4  38824  dihmeetlem1N  42539  modelaxreplem1  46163  fmtnofac2lem  48858  2itscp  50098  mofsn  50160