Theorem syld3an2 1411

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 1371	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 206  df-an 397  df-3an 1089

This theorem is referenced by:  enfii  9140  domsdomtrfi  9156  nppcan2  11441  nnncan  11445  nnncan2  11447  subdivcomb2  11860  ltdivmul  12039  ledivmul  12040  ltdiv23  12055  lediv23  12056  xrmaxlt  13110  xrltmin  13111  xrmaxle  13112  xrlemin  13113  pfxtrcfv  14593  pfxco  14739  dvdssub2  16194  dvdsgcdb  16437  lcmdvdsb  16500  vdwapun  16857  poslubdg  18317  ipodrsfi  18442  mulginvcom  18915  matinvgcell  21821  mdetrsca2  21990  mdetrlin2  21993  mdetunilem5  22002  decpmatmul  22158  islp3  22534  bddibl  25241  nvpi  29672  nvabs  29677  nmmulg  32638  lineid  34744  oplecon1b  37736  opltcon1b  37740  oldmm2  37753  oldmj2  37757  cmt3N  37786  2llnneN  37945  cvrexchlem  37955  pmod2iN  38385  polcon2N  38455  paddatclN  38485  osumcllem3N  38494  ltrnval1  38670  cdleme48fv  39035  cdlemg33b  39243  trlcolem  39262  cdlemh  39353  cdlemi1  39354  cdlemi2  39355  cdlemi  39356  cdlemk4  39370  cdlemk19u1  39505  cdlemn3  39733  hgmapfval  40422  pell14qrgap  41256  mnringmulrcld  42630  stoweidlem22  44383  stoweidlem26  44387  sigarexp  45220  lindszr  46670  fv2arycl  46854