Theorem syld3an2 1407

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  nppcan2  10911  nnncan  10915  nnncan2  10917  subdivcomb2  11330  ltdivmul  11509  ledivmul  11510  ltdiv23  11525  lediv23  11526  xrmaxlt  12568  xrltmin  12569  xrmaxle  12570  xrlemin  12571  pfxtrcfv  14049  pfxco  14194  dvdssub2  15645  dvdsgcdb  15887  lcmdvdsb  15951  vdwapun  16304  poslubdg  17753  ipodrsfi  17767  mulginvcom  18246  matinvgcell  21038  mdetrsca2  21207  mdetrlin2  21210  mdetunilem5  21219  decpmatmul  21374  islp3  21748  bddibl  24434  nvpi  28438  nvabs  28443  nmmulg  31204  lineid  33539  oplecon1b  36331  opltcon1b  36335  oldmm2  36348  oldmj2  36352  cmt3N  36381  2llnneN  36539  cvrexchlem  36549  pmod2iN  36979  polcon2N  37049  paddatclN  37079  osumcllem3N  37088  ltrnval1  37264  cdleme48fv  37629  cdlemg33b  37837  trlcolem  37856  cdlemh  37947  cdlemi1  37948  cdlemi2  37949  cdlemi  37950  cdlemk4  37964  cdlemk19u1  38099  cdlemn3  38327  hgmapfval  39016  pell14qrgap  39465  stoweidlem22  42301  stoweidlem26  42305  sigarexp  43110  lindszr  44518