Theorem syld3an2 1409

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  enfii  8932  domtrfi  8938  nppcan2  11182  nnncan  11186  nnncan2  11188  subdivcomb2  11601  ltdivmul  11780  ledivmul  11781  ltdiv23  11796  lediv23  11797  xrmaxlt  12844  xrltmin  12845  xrmaxle  12846  xrlemin  12847  pfxtrcfv  14334  pfxco  14479  dvdssub2  15938  dvdsgcdb  16181  lcmdvdsb  16246  vdwapun  16603  poslubdg  18047  ipodrsfi  18172  mulginvcom  18643  matinvgcell  21492  mdetrsca2  21661  mdetrlin2  21664  mdetunilem5  21673  decpmatmul  21829  islp3  22205  bddibl  24909  nvpi  28930  nvabs  28935  nmmulg  31818  lineid  34312  oplecon1b  37142  opltcon1b  37146  oldmm2  37159  oldmj2  37163  cmt3N  37192  2llnneN  37350  cvrexchlem  37360  pmod2iN  37790  polcon2N  37860  paddatclN  37890  osumcllem3N  37899  ltrnval1  38075  cdleme48fv  38440  cdlemg33b  38648  trlcolem  38667  cdlemh  38758  cdlemi1  38759  cdlemi2  38760  cdlemi  38761  cdlemk4  38775  cdlemk19u1  38910  cdlemn3  39138  hgmapfval  39827  pell14qrgap  40613  mnringmulrcld  41735  stoweidlem22  43453  stoweidlem26  43457  sigarexp  44262  lindszr  45698  fv2arycl  45882