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  9173  domsdomtrfi  9189  nppcan2  11500  nnncan  11504  nnncan2  11506  div11  11911  subdivcomb2  11922  ltdivmul  12101  ledivmul  12102  ltdiv23  12117  lediv23  12118  xrmaxlt  13219  xrltmin  13220  xrmaxle  13221  xrlemin  13222  pfxtrcfv  14748  pfxco  14895  dvdssub2  16377  dvdsgcdb  16621  lcmdvdsb  16689  vdwapun  17052  poslubdg  18486  ipodrsfi  18613  mulginvcom  19189  matinvgcell  22622  mdetrsca2  22791  mdetrlin2  22794  mdetunilem5  22803  decpmatmul  22959  islp3  23333  bddibl  26030  nvpi  31066  nvabs  31071  nmmulg  34396  fineqvnttrclselem2  35568  fineqvnttrclselem3  35569  lineid  36588  oplecon1b  40008  opltcon1b  40012  oldmm2  40025  oldmj2  40029  cmt3N  40058  2llnneN  40216  cvrexchlem  40226  pmod2iN  40656  polcon2N  40726  paddatclN  40756  osumcllem3N  40765  ltrnval1  40941  cdleme48fv  41306  cdlemg33b  41514  trlcolem  41533  cdlemh  41624  cdlemi1  41625  cdlemi2  41626  cdlemi  41627  cdlemk4  41641  cdlemk19u1  41776  cdlemn3  42004  hgmapfval  42693  pell14qrgap  43635  mnringmulrcld  44985  stoweidlem22  46769  stoweidlem26  46773  sigarexp  47606  lindszr  49282  fv2arycl  49461