Theorem syld3an2 1438

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  enfii  9166  domsdomtrfi  9182  nppcan2  11484  nnncan  11488  nnncan2  11490  div11  11895  subdivcomb2  11906  ltdivmul  12085  ledivmul  12086  ltdiv23  12101  lediv23  12102  xrmaxlt  13202  xrltmin  13203  xrmaxle  13204  xrlemin  13205  pfxtrcfv  14726  pfxco  14871  dvdssub2  16354  dvdsgcdb  16598  lcmdvdsb  16666  vdwapun  17029  poslubdg  18463  ipodrsfi  18590  mulginvcom  19160  matinvgcell  22592  mdetrsca2  22761  mdetrlin2  22764  mdetunilem5  22773  decpmatmul  22929  islp3  23303  bddibl  25999  nvpi  31019  nvabs  31024  nmmulg  34356  fineqvnttrclselem2  35535  fineqvnttrclselem3  35536  lineid  36575  oplecon1b  39975  opltcon1b  39979  oldmm2  39992  oldmj2  39996  cmt3N  40025  2llnneN  40183  cvrexchlem  40193  pmod2iN  40623  polcon2N  40693  paddatclN  40723  osumcllem3N  40732  ltrnval1  40908  cdleme48fv  41273  cdlemg33b  41481  trlcolem  41500  cdlemh  41591  cdlemi1  41592  cdlemi2  41593  cdlemi  41594  cdlemk4  41608  cdlemk19u1  41743  cdlemn3  41971  hgmapfval  42660  pell14qrgap  43602  mnringmulrcld  44952  stoweidlem22  46736  stoweidlem26  46740  sigarexp  47573  lindszr  49249  fv2arycl  49428