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  9198  domsdomtrfi  9214  nppcan2  11512  nnncan  11516  nnncan2  11518  div11  11922  subdivcomb2  11935  ltdivmul  12115  ledivmul  12116  ltdiv23  12131  lediv23  12132  xrmaxlt  13195  xrltmin  13196  xrmaxle  13197  xrlemin  13198  pfxtrcfv  14709  pfxco  14855  dvdssub2  16318  dvdsgcdb  16562  lcmdvdsb  16630  vdwapun  16992  poslubdg  18422  ipodrsfi  18547  mulginvcom  19080  matinvgcell  22371  mdetrsca2  22540  mdetrlin2  22543  mdetunilem5  22552  decpmatmul  22708  islp3  23082  bddibl  25791  nvpi  30594  nvabs  30599  nmmulg  33943  lineid  36047  oplecon1b  39165  opltcon1b  39169  oldmm2  39182  oldmj2  39186  cmt3N  39215  2llnneN  39374  cvrexchlem  39384  pmod2iN  39814  polcon2N  39884  paddatclN  39914  osumcllem3N  39923  ltrnval1  40099  cdleme48fv  40464  cdlemg33b  40672  trlcolem  40691  cdlemh  40782  cdlemi1  40783  cdlemi2  40784  cdlemi  40785  cdlemk4  40799  cdlemk19u1  40934  cdlemn3  41162  hgmapfval  41851  pell14qrgap  42845  mnringmulrcld  44200  stoweidlem22  45999  stoweidlem26  46003  sigarexp  46836  lindszr  48393  fv2arycl  48576