Theorem syl2and 607

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 604	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂))
5	1, 4	syland 602	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 206  df-an 396

This theorem is referenced by:  anim12d  608  ax7  2012  dffi3  9448  cflim2  10280  axpre-sup  11186  xle2add  13264  fzen  13544  rpmulgcd2  16620  pcqmul  16815  sbcie2s  17123  initoeu1  17993  termoeu1  18000  plttr  18327  pospo  18330  lublecllem  18345  latjlej12  18440  latmlem12  18456  hausnei2  23250  uncmp  23300  itgsubst  25977  mpodvdsmulf1o  27119  dvdsmulf1o  27121  2sqlem8a  27351  precsexlem10  28107  axcontlem9  28776  uspgr2wlkeq  29453  shintcli  31132  cvntr  32095  cdj3i  32244  f1resrcmplf1dlem  34703  satffunlem  35005  bj-bary1  36785  heicant  37122  itg2addnc  37141  dihmeetlem1N  40757  fmtnofac2lem  46902  2itscp  47848  mofsn  47890

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »