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  9090  domsdomtrfi  9106  nppcan2  11387  nnncan  11391  nnncan2  11393  div11  11799  subdivcomb2  11812  ltdivmul  11992  ledivmul  11993  ltdiv23  12008  lediv23  12009  xrmaxlt  13075  xrltmin  13076  xrmaxle  13077  xrlemin  13078  pfxtrcfv  14595  pfxco  14740  dvdssub2  16207  dvdsgcdb  16451  lcmdvdsb  16519  vdwapun  16881  poslubdg  18313  ipodrsfi  18440  mulginvcom  19007  matinvgcell  22345  mdetrsca2  22514  mdetrlin2  22517  mdetunilem5  22526  decpmatmul  22682  islp3  23056  bddibl  25763  nvpi  30639  nvabs  30644  nmmulg  33971  fineqvnttrclselem2  35134  fineqvnttrclselem3  35135  lineid  36117  oplecon1b  39240  opltcon1b  39244  oldmm2  39257  oldmj2  39261  cmt3N  39290  2llnneN  39448  cvrexchlem  39458  pmod2iN  39888  polcon2N  39958  paddatclN  39988  osumcllem3N  39997  ltrnval1  40173  cdleme48fv  40538  cdlemg33b  40746  trlcolem  40765  cdlemh  40856  cdlemi1  40857  cdlemi2  40858  cdlemi  40859  cdlemk4  40873  cdlemk19u1  41008  cdlemn3  41236  hgmapfval  41925  pell14qrgap  42908  mnringmulrcld  44261  stoweidlem22  46060  stoweidlem26  46064  sigarexp  46897  lindszr  48501  fv2arycl  48680