Theorem syld3an2 1408

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  nppcan2  10906  nnncan  10910  nnncan2  10912  subdivcomb2  11325  ltdivmul  11504  ledivmul  11505  ltdiv23  11520  lediv23  11521  xrmaxlt  12562  xrltmin  12563  xrmaxle  12564  xrlemin  12565  pfxtrcfv  14046  pfxco  14191  dvdssub2  15643  dvdsgcdb  15883  lcmdvdsb  15947  vdwapun  16300  poslubdg  17751  ipodrsfi  17765  mulginvcom  18244  matinvgcell  21040  mdetrsca2  21209  mdetrlin2  21212  mdetunilem5  21221  decpmatmul  21377  islp3  21751  bddibl  24443  nvpi  28450  nvabs  28455  nmmulg  31319  lineid  33657  oplecon1b  36497  opltcon1b  36501  oldmm2  36514  oldmj2  36518  cmt3N  36547  2llnneN  36705  cvrexchlem  36715  pmod2iN  37145  polcon2N  37215  paddatclN  37245  osumcllem3N  37254  ltrnval1  37430  cdleme48fv  37795  cdlemg33b  38003  trlcolem  38022  cdlemh  38113  cdlemi1  38114  cdlemi2  38115  cdlemi  38116  cdlemk4  38130  cdlemk19u1  38265  cdlemn3  38493  hgmapfval  39182  pell14qrgap  39816  mnringmulrcld  40936  stoweidlem22  42664  stoweidlem26  42668  sigarexp  43473  lindszr  44878  fv2arycl  45062