Theorem syld3an2 1410

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 1135	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑)
2		syld3an2.1	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3		simp3 1137	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃)
4		syld3an2.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1370	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  9223  domsdomtrfi  9239  nppcan2  11537  nnncan  11541  nnncan2  11543  div11  11947  subdivcomb2  11960  ltdivmul  12140  ledivmul  12141  ltdiv23  12156  lediv23  12157  xrmaxlt  13219  xrltmin  13220  xrmaxle  13221  xrlemin  13222  pfxtrcfv  14727  pfxco  14873  dvdssub2  16334  dvdsgcdb  16578  lcmdvdsb  16646  vdwapun  17007  poslubdg  18471  ipodrsfi  18596  mulginvcom  19129  matinvgcell  22456  mdetrsca2  22625  mdetrlin2  22628  mdetunilem5  22637  decpmatmul  22793  islp3  23169  bddibl  25889  nvpi  30695  nvabs  30700  nmmulg  33928  lineid  36064  oplecon1b  39182  opltcon1b  39186  oldmm2  39199  oldmj2  39203  cmt3N  39232  2llnneN  39391  cvrexchlem  39401  pmod2iN  39831  polcon2N  39901  paddatclN  39931  osumcllem3N  39940  ltrnval1  40116  cdleme48fv  40481  cdlemg33b  40689  trlcolem  40708  cdlemh  40799  cdlemi1  40800  cdlemi2  40801  cdlemi  40802  cdlemk4  40816  cdlemk19u1  40951  cdlemn3  41179  hgmapfval  41868  pell14qrgap  42862  mnringmulrcld  44223  stoweidlem22  45977  stoweidlem26  45981  sigarexp  46814  lindszr  48314  fv2arycl  48497