Theorem syld3an2 1413

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 1136	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑)
2		syld3an2.1	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3		simp3 1138	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃)
4		syld3an2.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1373	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  enfii  9110  domsdomtrfi  9126  nppcan2  11412  nnncan  11416  nnncan2  11418  div11  11824  subdivcomb2  11837  ltdivmul  12017  ledivmul  12018  ltdiv23  12033  lediv23  12034  xrmaxlt  13096  xrltmin  13097  xrmaxle  13098  xrlemin  13099  pfxtrcfv  14616  pfxco  14761  dvdssub2  16228  dvdsgcdb  16472  lcmdvdsb  16540  vdwapun  16902  poslubdg  18335  ipodrsfi  18462  mulginvcom  19029  matinvgcell  22379  mdetrsca2  22548  mdetrlin2  22551  mdetunilem5  22560  decpmatmul  22716  islp3  23090  bddibl  25797  nvpi  30742  nvabs  30747  nmmulg  34123  fineqvnttrclselem2  35278  fineqvnttrclselem3  35279  lineid  36277  oplecon1b  39461  opltcon1b  39465  oldmm2  39478  oldmj2  39482  cmt3N  39511  2llnneN  39669  cvrexchlem  39679  pmod2iN  40109  polcon2N  40179  paddatclN  40209  osumcllem3N  40218  ltrnval1  40394  cdleme48fv  40759  cdlemg33b  40967  trlcolem  40986  cdlemh  41077  cdlemi1  41078  cdlemi2  41079  cdlemi  41080  cdlemk4  41094  cdlemk19u1  41229  cdlemn3  41457  hgmapfval  42146  pell14qrgap  43117  mnringmulrcld  44469  stoweidlem22  46266  stoweidlem26  46270  sigarexp  47103  lindszr  48715  fv2arycl  48894