Theorem syld3an2 1411

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 1371	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  enfii  9252  domsdomtrfi  9268  nppcan2  11567  nnncan  11571  nnncan2  11573  div11  11977  subdivcomb2  11990  ltdivmul  12170  ledivmul  12171  ltdiv23  12186  lediv23  12187  xrmaxlt  13243  xrltmin  13244  xrmaxle  13245  xrlemin  13246  pfxtrcfv  14741  pfxco  14887  dvdssub2  16349  dvdsgcdb  16592  lcmdvdsb  16660  vdwapun  17021  poslubdg  18484  ipodrsfi  18609  mulginvcom  19139  matinvgcell  22462  mdetrsca2  22631  mdetrlin2  22634  mdetunilem5  22643  decpmatmul  22799  islp3  23175  bddibl  25895  nvpi  30699  nvabs  30704  nmmulg  33914  lineid  36047  oplecon1b  39157  opltcon1b  39161  oldmm2  39174  oldmj2  39178  cmt3N  39207  2llnneN  39366  cvrexchlem  39376  pmod2iN  39806  polcon2N  39876  paddatclN  39906  osumcllem3N  39915  ltrnval1  40091  cdleme48fv  40456  cdlemg33b  40664  trlcolem  40683  cdlemh  40774  cdlemi1  40775  cdlemi2  40776  cdlemi  40777  cdlemk4  40791  cdlemk19u1  40926  cdlemn3  41154  hgmapfval  41843  pell14qrgap  42831  mnringmulrcld  44197  stoweidlem22  45943  stoweidlem26  45947  sigarexp  46780  lindszr  48198  fv2arycl  48382