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  9156  domsdomtrfi  9172  nppcan2  11460  nnncan  11464  nnncan2  11466  div11  11872  subdivcomb2  11885  ltdivmul  12065  ledivmul  12066  ltdiv23  12081  lediv23  12082  xrmaxlt  13148  xrltmin  13149  xrmaxle  13150  xrlemin  13151  pfxtrcfv  14665  pfxco  14811  dvdssub2  16278  dvdsgcdb  16522  lcmdvdsb  16590  vdwapun  16952  poslubdg  18380  ipodrsfi  18505  mulginvcom  19038  matinvgcell  22329  mdetrsca2  22498  mdetrlin2  22501  mdetunilem5  22510  decpmatmul  22666  islp3  23040  bddibl  25748  nvpi  30603  nvabs  30608  nmmulg  33963  lineid  36078  oplecon1b  39201  opltcon1b  39205  oldmm2  39218  oldmj2  39222  cmt3N  39251  2llnneN  39410  cvrexchlem  39420  pmod2iN  39850  polcon2N  39920  paddatclN  39950  osumcllem3N  39959  ltrnval1  40135  cdleme48fv  40500  cdlemg33b  40708  trlcolem  40727  cdlemh  40818  cdlemi1  40819  cdlemi2  40820  cdlemi  40821  cdlemk4  40835  cdlemk19u1  40970  cdlemn3  41198  hgmapfval  41887  pell14qrgap  42870  mnringmulrcld  44224  stoweidlem22  46027  stoweidlem26  46031  sigarexp  46864  lindszr  48462  fv2arycl  48641