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  9090  domsdomtrfi  9106  nppcan2  11384  nnncan  11388  nnncan2  11390  div11  11796  subdivcomb2  11809  ltdivmul  11989  ledivmul  11990  ltdiv23  12005  lediv23  12006  xrmaxlt  13072  xrltmin  13073  xrmaxle  13074  xrlemin  13075  pfxtrcfv  14592  pfxco  14737  dvdssub2  16204  dvdsgcdb  16448  lcmdvdsb  16516  vdwapun  16878  poslubdg  18310  ipodrsfi  18437  mulginvcom  19004  matinvgcell  22343  mdetrsca2  22512  mdetrlin2  22515  mdetunilem5  22524  decpmatmul  22680  islp3  23054  bddibl  25761  nvpi  30637  nvabs  30642  nmmulg  33969  fineqvnttrclselem2  35110  fineqvnttrclselem3  35111  lineid  36096  oplecon1b  39219  opltcon1b  39223  oldmm2  39236  oldmj2  39240  cmt3N  39269  2llnneN  39427  cvrexchlem  39437  pmod2iN  39867  polcon2N  39937  paddatclN  39967  osumcllem3N  39976  ltrnval1  40152  cdleme48fv  40517  cdlemg33b  40725  trlcolem  40744  cdlemh  40835  cdlemi1  40836  cdlemi2  40837  cdlemi  40838  cdlemk4  40852  cdlemk19u1  40987  cdlemn3  41215  hgmapfval  41904  pell14qrgap  42887  mnringmulrcld  44240  stoweidlem22  46039  stoweidlem26  46043  sigarexp  46876  lindszr  48480  fv2arycl  48659