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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  enfii  9194  domsdomtrfi  9210  nppcan2  11582  nnncan  11586  nnncan2  11588  div11  11995  subdivcomb2  12006  ltdivmul  12185  ledivmul  12186  ltdiv23  12201  lediv23  12202  xrmaxlt  13304  xrltmin  13305  xrmaxle  13306  xrlemin  13307  pfxtrcfv  14835  pfxco  14982  dvdssub2  16464  dvdsgcdb  16711  lcmdvdsb  16781  vdwapun  17145  poslubdg  18579  ipodrsfi  18706  mulginvcom  19302  matinvgcell  22743  mdetrsca2  22912  mdetrlin2  22915  mdetunilem5  22924  decpmatmul  23083  islp3  23457  bddibl  26153  nvpi  31262  nvabs  31267  nmmulg  34591  fineqvnttrclselem2  35773  fineqvnttrclselem3  35774  lineid  36828  oplecon1b  40238  opltcon1b  40242  oldmm2  40255  oldmj2  40259  cmt3N  40288  2llnneN  40446  cvrexchlem  40456  pmod2iN  40886  polcon2N  40956  paddatclN  40986  osumcllem3N  40995  ltrnval1  41171  cdleme48fv  41536  cdlemg33b  41744  trlcolem  41763  cdlemh  41854  cdlemi1  41855  cdlemi2  41856  cdlemi  41857  cdlemk4  41871  cdlemk19u1  42006  cdlemn3  42234  hgmapfval  42923  pell14qrgap  43861  mnringmulrcld  45211  stoweidlem22  47001  stoweidlem26  47005  sigarexp  47838  lindszr  49550  fv2arycl  49729