Theorem syld3an2 1413

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 1136	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑)
2		syld3an2.1	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3		simp3 1138	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃)
4		syld3an2.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

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

This theorem is referenced by:  enfii  9106  domsdomtrfi  9122  nppcan2  11403  nnncan  11407  nnncan2  11409  div11  11815  subdivcomb2  11828  ltdivmul  12008  ledivmul  12009  ltdiv23  12024  lediv23  12025  xrmaxlt  13087  xrltmin  13088  xrmaxle  13089  xrlemin  13090  pfxtrcfv  14607  pfxco  14752  dvdssub2  16219  dvdsgcdb  16463  lcmdvdsb  16531  vdwapun  16893  poslubdg  18326  ipodrsfi  18453  mulginvcom  19020  matinvgcell  22370  mdetrsca2  22539  mdetrlin2  22542  mdetunilem5  22551  decpmatmul  22707  islp3  23081  bddibl  25788  nvpi  30668  nvabs  30673  nmmulg  34051  fineqvnttrclselem2  35214  fineqvnttrclselem3  35215  lineid  36199  oplecon1b  39373  opltcon1b  39377  oldmm2  39390  oldmj2  39394  cmt3N  39423  2llnneN  39581  cvrexchlem  39591  pmod2iN  40021  polcon2N  40091  paddatclN  40121  osumcllem3N  40130  ltrnval1  40306  cdleme48fv  40671  cdlemg33b  40879  trlcolem  40898  cdlemh  40989  cdlemi1  40990  cdlemi2  40991  cdlemi  40992  cdlemk4  41006  cdlemk19u1  41141  cdlemn3  41369  hgmapfval  42058  pell14qrgap  43032  mnringmulrcld  44385  stoweidlem22  46182  stoweidlem26  46186  sigarexp  47019  lindszr  48631  fv2arycl  48810