Theorem syld3an2 1438

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

Ref	Expression
syld3an2.1	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
syld3an2.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syld3an2	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Proof of Theorem syld3an2

Step	Hyp	Ref	Expression
1		simp1 1154	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑)
2		syld3an2.1	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3		simp3 1156	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃)
4		syld3an2.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

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  df-3an 1105

This theorem is used by:  enfii  9205  domsdomtrfi  9221  nppcan2  11593  nnncan  11597  nnncan2  11599  div11  12006  subdivcomb2  12017  ltdivmul  12196  ledivmul  12197  ltdiv23  12212  lediv23  12213  xrmaxlt  13315  xrltmin  13316  xrmaxle  13317  xrlemin  13318  pfxtrcfv  14847  pfxco  14994  dvdssub2  16477  dvdsgcdb  16724  lcmdvdsb  16794  vdwapun  17158  poslubdg  18592  ipodrsfi  18719  mulginvcom  19315  matinvgcell  22756  mdetrsca2  22925  mdetrlin2  22928  mdetunilem5  22937  decpmatmul  23096  islp3  23470  bddibl  26166  nvpi  31275  nvabs  31280  nmmulg  34645  fineqvnttrclselem2  35847  fineqvnttrclselem3  35848  lineid  36941  oplecon1b  40352  opltcon1b  40356  oldmm2  40369  oldmj2  40373  cmt3N  40402  2llnneN  40560  cvrexchlem  40570  pmod2iN  41000  polcon2N  41070  paddatclN  41100  osumcllem3N  41109  ltrnval1  41285  cdleme48fv  41650  cdlemg33b  41858  trlcolem  41877  cdlemh  41968  cdlemi1  41969  cdlemi2  41970  cdlemi  41971  cdlemk4  41985  cdlemk19u1  42120  cdlemn3  42348  hgmapfval  43037  pell14qrgap  43976  mnringmulrcld  45320  stoweidlem22  47126  stoweidlem26  47130  sigarexp  47963  lindszr  49675  fv2arycl  49854