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  9110  domsdomtrfi  9126  nppcan2  11414  nnncan  11418  nnncan2  11420  div11  11826  subdivcomb2  11839  ltdivmul  12019  ledivmul  12020  ltdiv23  12035  lediv23  12036  xrmaxlt  13102  xrltmin  13103  xrmaxle  13104  xrlemin  13105  pfxtrcfv  14618  pfxco  14764  dvdssub2  16231  dvdsgcdb  16475  lcmdvdsb  16543  vdwapun  16905  poslubdg  18337  ipodrsfi  18464  mulginvcom  18997  matinvgcell  22339  mdetrsca2  22508  mdetrlin2  22511  mdetunilem5  22520  decpmatmul  22676  islp3  23050  bddibl  25758  nvpi  30630  nvabs  30635  nmmulg  33952  lineid  36076  oplecon1b  39199  opltcon1b  39203  oldmm2  39216  oldmj2  39220  cmt3N  39249  2llnneN  39408  cvrexchlem  39418  pmod2iN  39848  polcon2N  39918  paddatclN  39948  osumcllem3N  39957  ltrnval1  40133  cdleme48fv  40498  cdlemg33b  40706  trlcolem  40725  cdlemh  40816  cdlemi1  40817  cdlemi2  40818  cdlemi  40819  cdlemk4  40833  cdlemk19u1  40968  cdlemn3  41196  hgmapfval  41885  pell14qrgap  42868  mnringmulrcld  44221  stoweidlem22  46023  stoweidlem26  46027  sigarexp  46860  lindszr  48474  fv2arycl  48653