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  9201  domsdomtrfi  9217  nppcan2  11589  nnncan  11593  nnncan2  11595  div11  12002  subdivcomb2  12013  ltdivmul  12192  ledivmul  12193  ltdiv23  12208  lediv23  12209  xrmaxlt  13311  xrltmin  13312  xrmaxle  13313  xrlemin  13314  pfxtrcfv  14842  pfxco  14989  dvdssub2  16471  dvdsgcdb  16718  lcmdvdsb  16788  vdwapun  17152  poslubdg  18586  ipodrsfi  18713  mulginvcom  19309  matinvgcell  22750  mdetrsca2  22919  mdetrlin2  22922  mdetunilem5  22931  decpmatmul  23090  islp3  23464  bddibl  26160  nvpi  31269  nvabs  31274  nmmulg  34598  fineqvnttrclselem2  35790  fineqvnttrclselem3  35791  lineid  36848  oplecon1b  40259  opltcon1b  40263  oldmm2  40276  oldmj2  40280  cmt3N  40309  2llnneN  40467  cvrexchlem  40477  pmod2iN  40907  polcon2N  40977  paddatclN  41007  osumcllem3N  41016  ltrnval1  41192  cdleme48fv  41557  cdlemg33b  41765  trlcolem  41784  cdlemh  41875  cdlemi1  41876  cdlemi2  41877  cdlemi  41878  cdlemk4  41892  cdlemk19u1  42027  cdlemn3  42255  hgmapfval  42944  pell14qrgap  43882  mnringmulrcld  45226  stoweidlem22  47032  stoweidlem26  47036  sigarexp  47869  lindszr  49581  fv2arycl  49760