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  9127  domsdomtrfi  9143  nppcan2  11429  nnncan  11433  nnncan2  11435  div11  11841  subdivcomb2  11854  ltdivmul  12034  ledivmul  12035  ltdiv23  12050  lediv23  12051  xrmaxlt  13117  xrltmin  13118  xrmaxle  13119  xrlemin  13120  pfxtrcfv  14634  pfxco  14780  dvdssub2  16247  dvdsgcdb  16491  lcmdvdsb  16559  vdwapun  16921  poslubdg  18349  ipodrsfi  18474  mulginvcom  19007  matinvgcell  22298  mdetrsca2  22467  mdetrlin2  22470  mdetunilem5  22479  decpmatmul  22635  islp3  23009  bddibl  25717  nvpi  30569  nvabs  30574  nmmulg  33929  lineid  36044  oplecon1b  39167  opltcon1b  39171  oldmm2  39184  oldmj2  39188  cmt3N  39217  2llnneN  39376  cvrexchlem  39386  pmod2iN  39816  polcon2N  39886  paddatclN  39916  osumcllem3N  39925  ltrnval1  40101  cdleme48fv  40466  cdlemg33b  40674  trlcolem  40693  cdlemh  40784  cdlemi1  40785  cdlemi2  40786  cdlemi  40787  cdlemk4  40801  cdlemk19u1  40936  cdlemn3  41164  hgmapfval  41853  pell14qrgap  42836  mnringmulrcld  44190  stoweidlem22  45993  stoweidlem26  45997  sigarexp  46830  lindszr  48431  fv2arycl  48610