Theorem syld3an2 1436

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  enfii  9166  domsdomtrfi  9182  nppcan2  11485  nnncan  11489  nnncan2  11491  div11  11896  subdivcomb2  11907  ltdivmul  12086  ledivmul  12087  ltdiv23  12102  lediv23  12103  xrmaxlt  13203  xrltmin  13204  xrmaxle  13205  xrlemin  13206  pfxtrcfv  14726  pfxco  14871  dvdssub2  16355  dvdsgcdb  16599  lcmdvdsb  16667  vdwapun  17030  poslubdg  18464  ipodrsfi  18591  mulginvcom  19161  matinvgcell  22557  mdetrsca2  22726  mdetrlin2  22729  mdetunilem5  22738  decpmatmul  22894  islp3  23268  bddibl  25964  nvpi  30956  nvabs  30961  nmmulg  34297  fineqvnttrclselem2  35454  fineqvnttrclselem3  35455  lineid  36470  oplecon1b  39860  opltcon1b  39864  oldmm2  39877  oldmj2  39881  cmt3N  39910  2llnneN  40068  cvrexchlem  40078  pmod2iN  40508  polcon2N  40578  paddatclN  40608  osumcllem3N  40617  ltrnval1  40793  cdleme48fv  41158  cdlemg33b  41366  trlcolem  41385  cdlemh  41476  cdlemi1  41477  cdlemi2  41478  cdlemi  41479  cdlemk4  41493  cdlemk19u1  41628  cdlemn3  41856  hgmapfval  42545  pell14qrgap  43489  mnringmulrcld  44839  stoweidlem22  46623  stoweidlem26  46627  sigarexp  47460  lindszr  49129  fv2arycl  49308