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

This theorem is referenced by:  enfii  8981  domsdomtrfi  8997  nppcan2  11261  nnncan  11265  nnncan2  11267  subdivcomb2  11680  ltdivmul  11859  ledivmul  11860  ltdiv23  11875  lediv23  11876  xrmaxlt  12924  xrltmin  12925  xrmaxle  12926  xrlemin  12927  pfxtrcfv  14415  pfxco  14560  dvdssub2  16019  dvdsgcdb  16262  lcmdvdsb  16327  vdwapun  16684  poslubdg  18141  ipodrsfi  18266  mulginvcom  18737  matinvgcell  21593  mdetrsca2  21762  mdetrlin2  21765  mdetunilem5  21774  decpmatmul  21930  islp3  22306  bddibl  25013  nvpi  29038  nvabs  29043  nmmulg  31927  lineid  34394  oplecon1b  37222  opltcon1b  37226  oldmm2  37239  oldmj2  37243  cmt3N  37272  2llnneN  37430  cvrexchlem  37440  pmod2iN  37870  polcon2N  37940  paddatclN  37970  osumcllem3N  37979  ltrnval1  38155  cdleme48fv  38520  cdlemg33b  38728  trlcolem  38747  cdlemh  38838  cdlemi1  38839  cdlemi2  38840  cdlemi  38841  cdlemk4  38855  cdlemk19u1  38990  cdlemn3  39218  hgmapfval  39907  pell14qrgap  40704  mnringmulrcld  41853  stoweidlem22  43570  stoweidlem26  43574  sigarexp  44386  lindszr  45821  fv2arycl  46005