Theorem syld3an2 1412

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  enfii  9189  domsdomtrfi  9205  nppcan2  11491  nnncan  11495  nnncan2  11497  subdivcomb2  11910  ltdivmul  12089  ledivmul  12090  ltdiv23  12105  lediv23  12106  xrmaxlt  13160  xrltmin  13161  xrmaxle  13162  xrlemin  13163  pfxtrcfv  14643  pfxco  14789  dvdssub2  16244  dvdsgcdb  16487  lcmdvdsb  16550  vdwapun  16907  poslubdg  18367  ipodrsfi  18492  mulginvcom  18979  matinvgcell  21937  mdetrsca2  22106  mdetrlin2  22109  mdetunilem5  22118  decpmatmul  22274  islp3  22650  bddibl  25357  nvpi  29920  nvabs  29925  nmmulg  32948  lineid  35055  oplecon1b  38071  opltcon1b  38075  oldmm2  38088  oldmj2  38092  cmt3N  38121  2llnneN  38280  cvrexchlem  38290  pmod2iN  38720  polcon2N  38790  paddatclN  38820  osumcllem3N  38829  ltrnval1  39005  cdleme48fv  39370  cdlemg33b  39578  trlcolem  39597  cdlemh  39688  cdlemi1  39689  cdlemi2  39690  cdlemi  39691  cdlemk4  39705  cdlemk19u1  39840  cdlemn3  40068  hgmapfval  40757  pell14qrgap  41613  mnringmulrcld  42987  stoweidlem22  44738  stoweidlem26  44742  sigarexp  45575  lindszr  47150  fv2arycl  47334