Theorem syld3an2 1519

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

Syntax hints:   → wi 4   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  nppcan2  10502  nnncan  10506  nnncan2  10508  ltdivmul  11088  ledivmul  11089  ltdiv23  11104  lediv23  11105  xrmaxlt  12203  xrltmin  12204  xrmaxle  12205  xrlemin  12206  swrdtrcfv  13639  dvdssub2  15223  dvdsgcdb  15462  lcmdvdsb  15526  vdwapun  15878  poslubdg  17348  ipodrsfi  17362  mulginvcom  17764  matinvgcell  20441  mdetrsca2  20610  mdetrlin2  20613  mdetunilem5  20622  decpmatmul  20777  islp3  21150  bddibl  23803  nvpi  27829  nvabs  27834  nmmulg  30319  subdivcomb2  31917  lineid  32494  oplecon1b  34989  opltcon1b  34993  oldmm2  35006  oldmj2  35010  cmt3N  35039  2llnneN  35196  cvrexchlem  35206  pmod2iN  35636  polcon2N  35706  paddatclN  35736  osumcllem3N  35745  ltrnval1  35921  cdleme48fv  36287  cdlemg33b  36495  trlcolem  36514  cdlemh  36605  cdlemi1  36606  cdlemi2  36607  cdlemi  36608  cdlemk4  36622  cdlemk19u1  36757  cdlemn3  36986  hgmapfval  37678  pell14qrgap  37939  stoweidlem22  40740  stoweidlem26  40744  sigarexp  41552  pfxtrcfv  41909  pfxco  41946  lindszr  42766