Theorem syl2and 499

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  anim12d  585  ax7  1989  dffi3  8378  cflim2  9123  axpre-sup  10028  xle2add  12127  fzen  12396  rpmulgcd2  15417  pcqmul  15605  initoeu1  16708  termoeu1  16715  plttr  17017  pospo  17020  lublecllem  17035  latjlej12  17114  latmlem12  17130  cygabl  18338  hausnei2  21205  uncmp  21254  itgsubst  23857  dvdsmulf1o  24965  2sqlem8a  25195  axcontlem9  25897  uspgr2wlkeq  26598  shintcli  28316  cvntr  29279  cdj3i  29428  bj-bary1  33292  heicant  33574  itg2addnc  33594  dihmeetlem1N  36896  fmtnofac2lem  41805