Theorem syld3an2 1419

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  enfii  9110  domsdomtrfi  9126  nppcan2  11416  nnncan  11420  nnncan2  11422  div11  11828  subdivcomb2  11842  ltdivmul  12022  ledivmul  12023  ltdiv23  12038  lediv23  12039  xrmaxlt  13124  xrltmin  13125  xrmaxle  13126  xrlemin  13127  pfxtrcfv  14646  pfxco  14791  dvdssub2  16261  dvdsgcdb  16505  lcmdvdsb  16573  vdwapun  16936  poslubdg  18369  ipodrsfi  18496  mulginvcom  19066  matinvgcell  22418  mdetrsca2  22587  mdetrlin2  22590  mdetunilem5  22599  decpmatmul  22755  islp3  23129  bddibl  25825  nvpi  30756  nvabs  30761  nmmulg  34150  fineqvnttrclselem2  35303  fineqvnttrclselem3  35304  lineid  36311  oplecon1b  39693  opltcon1b  39697  oldmm2  39710  oldmj2  39714  cmt3N  39743  2llnneN  39901  cvrexchlem  39911  pmod2iN  40341  polcon2N  40411  paddatclN  40441  osumcllem3N  40450  ltrnval1  40626  cdleme48fv  40991  cdlemg33b  41199  trlcolem  41218  cdlemh  41309  cdlemi1  41310  cdlemi2  41311  cdlemi  41312  cdlemk4  41326  cdlemk19u1  41461  cdlemn3  41689  hgmapfval  42378  pell14qrgap  43320  mnringmulrcld  44672  stoweidlem22  46465  stoweidlem26  46469  sigarexp  47302  lindszr  48960  fv2arycl  49139