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

This theorem is referenced by:  enfii  8784  nppcan2  10995  nnncan  10999  nnncan2  11001  subdivcomb2  11414  ltdivmul  11593  ledivmul  11594  ltdiv23  11609  lediv23  11610  xrmaxlt  12657  xrltmin  12658  xrmaxle  12659  xrlemin  12660  pfxtrcfv  14144  pfxco  14289  dvdssub2  15746  dvdsgcdb  15989  lcmdvdsb  16054  vdwapun  16410  poslubdg  17875  ipodrsfi  17889  mulginvcom  18370  matinvgcell  21186  mdetrsca2  21355  mdetrlin2  21358  mdetunilem5  21367  decpmatmul  21523  islp3  21897  bddibl  24592  nvpi  28602  nvabs  28607  nmmulg  31488  lineid  34023  oplecon1b  36838  opltcon1b  36842  oldmm2  36855  oldmj2  36859  cmt3N  36888  2llnneN  37046  cvrexchlem  37056  pmod2iN  37486  polcon2N  37556  paddatclN  37586  osumcllem3N  37595  ltrnval1  37771  cdleme48fv  38136  cdlemg33b  38344  trlcolem  38363  cdlemh  38454  cdlemi1  38455  cdlemi2  38456  cdlemi  38457  cdlemk4  38471  cdlemk19u1  38606  cdlemn3  38834  hgmapfval  39523  pell14qrgap  40269  mnringmulrcld  41388  stoweidlem22  43105  stoweidlem26  43109  sigarexp  43914  lindszr  45344  fv2arycl  45528