Theorem syld3an2 1413

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  enfii  9150  domsdomtrfi  9166  nppcan2  11453  nnncan  11457  nnncan2  11459  div11  11865  subdivcomb2  11878  ltdivmul  12058  ledivmul  12059  ltdiv23  12074  lediv23  12075  xrmaxlt  13141  xrltmin  13142  xrmaxle  13143  xrlemin  13144  pfxtrcfv  14658  pfxco  14804  dvdssub2  16271  dvdsgcdb  16515  lcmdvdsb  16583  vdwapun  16945  poslubdg  18373  ipodrsfi  18498  mulginvcom  19031  matinvgcell  22322  mdetrsca2  22491  mdetrlin2  22494  mdetunilem5  22503  decpmatmul  22659  islp3  23033  bddibl  25741  nvpi  30596  nvabs  30601  nmmulg  33956  lineid  36071  oplecon1b  39194  opltcon1b  39198  oldmm2  39211  oldmj2  39215  cmt3N  39244  2llnneN  39403  cvrexchlem  39413  pmod2iN  39843  polcon2N  39913  paddatclN  39943  osumcllem3N  39952  ltrnval1  40128  cdleme48fv  40493  cdlemg33b  40701  trlcolem  40720  cdlemh  40811  cdlemi1  40812  cdlemi2  40813  cdlemi  40814  cdlemk4  40828  cdlemk19u1  40963  cdlemn3  41191  hgmapfval  41880  pell14qrgap  42863  mnringmulrcld  44217  stoweidlem22  46020  stoweidlem26  46024  sigarexp  46857  lindszr  48458  fv2arycl  48637