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 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  610  ax7  2018  dffi3  9335  cflim2  10174  axpre-sup  11081  xle2add  13200  fzen  13484  rpmulgcd2  16614  pcqmul  16813  sbcie2s  17120  initoeu1  17967  termoeu1  17974  plttr  18295  pospo  18298  lublecllem  18313  latjlej12  18410  latmlem12  18426  hausnei2  23327  uncmp  23377  itgsubst  26028  mpodvdsmulf1o  27175  dvdsmulf1o  27177  2sqlem8a  27407  precsexlem10  28227  axcontlem9  29060  uspgr2wlkeq  29734  shintcli  31420  cvntr  32383  cdj3i  32532  f1resrcmplf1dlem  35250  satffunlem  35604  bj-bary1  37639  heicant  37987  itg2addnc  38006  dihmeetlem1N  41747  modelaxreplem1  45420  fmtnofac2lem  48028  2itscp  49254  mofsn  49316