Theorem syld3an2 1414

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  enfii  9113  domsdomtrfi  9129  nppcan2  11416  nnncan  11420  nnncan2  11422  div11  11828  subdivcomb2  11842  ltdivmul  12022  ledivmul  12023  ltdiv23  12038  lediv23  12039  xrmaxlt  13124  xrltmin  13125  xrmaxle  13126  xrlemin  13127  pfxtrcfv  14646  pfxco  14791  dvdssub2  16261  dvdsgcdb  16505  lcmdvdsb  16573  vdwapun  16936  poslubdg  18369  ipodrsfi  18496  mulginvcom  19066  matinvgcell  22410  mdetrsca2  22579  mdetrlin2  22582  mdetunilem5  22591  decpmatmul  22747  islp3  23121  bddibl  25817  nvpi  30753  nvabs  30758  nmmulg  34126  fineqvnttrclselem2  35282  fineqvnttrclselem3  35283  lineid  36281  oplecon1b  39661  opltcon1b  39665  oldmm2  39678  oldmj2  39682  cmt3N  39711  2llnneN  39869  cvrexchlem  39879  pmod2iN  40309  polcon2N  40379  paddatclN  40409  osumcllem3N  40418  ltrnval1  40594  cdleme48fv  40959  cdlemg33b  41167  trlcolem  41186  cdlemh  41277  cdlemi1  41278  cdlemi2  41279  cdlemi  41280  cdlemk4  41294  cdlemk19u1  41429  cdlemn3  41657  hgmapfval  42346  pell14qrgap  43321  mnringmulrcld  44673  stoweidlem22  46468  stoweidlem26  46472  sigarexp  47305  lindszr  48957  fv2arycl  49136