Theorem syld3an2 1439

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 1399	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  9239  domsdomtrfi  9255  nppcan2  11628  nnncan  11632  nnncan2  11634  div11  12042  subdivcomb2  12053  ltdivmul  12232  ledivmul  12233  ltdiv23  12248  lediv23  12249  xrmaxlt  13351  xrltmin  13352  xrmaxle  13353  xrlemin  13354  pfxtrcfv  14884  pfxco  15031  dvdssub2  16515  dvdsgcdb  16762  lcmdvdsb  16832  vdwapun  17196  poslubdg  18636  ipodrsfi  18763  mulginvcom  19359  matinvgcell  22805  mdetrsca2  22974  mdetrlin2  22977  mdetunilem5  22986  decpmatmul  23145  islp3  23519  bddibl  26215  nvpi  31326  nvabs  31331  nmmulg  34709  fineqvnttrclselem2  35931  fineqvnttrclselem3  35932  lineid  37063  oplecon1b  40524  opltcon1b  40528  oldmm2  40541  oldmj2  40545  cmt3N  40574  2llnneN  40732  cvrexchlem  40742  pmod2iN  41172  polcon2N  41242  paddatclN  41272  osumcllem3N  41281  ltrnval1  41457  cdleme48fv  41822  cdlemg33b  42030  trlcolem  42049  cdlemh  42140  cdlemi1  42141  cdlemi2  42142  cdlemi  42143  cdlemk4  42157  cdlemk19u1  42292  cdlemn3  42520  hgmapfval  43209  pell14qrgap  44148  mnringmulrcld  45487  stoweidlem22  47305  stoweidlem26  47309  sigarexp  48142  linply2cfv  49712  lindszr  49912  fv2arycl  50091