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  10916  nnncan  10920  nnncan2  10922  subdivcomb2  11335  ltdivmul  11514  ledivmul  11515  ltdiv23  11530  lediv23  11531  xrmaxlt  12573  xrltmin  12574  xrmaxle  12575  xrlemin  12576  pfxtrcfv  14054  pfxco  14199  dvdssub2  15650  dvdsgcdb  15892  lcmdvdsb  15956  vdwapun  16309  poslubdg  17758  ipodrsfi  17772  mulginvcom  18251  matinvgcell  21043  mdetrsca2  21212  mdetrlin2  21215  mdetunilem5  21224  decpmatmul  21379  islp3  21753  bddibl  24439  nvpi  28443  nvabs  28448  nmmulg  31209  lineid  33544  oplecon1b  36336  opltcon1b  36340  oldmm2  36353  oldmj2  36357  cmt3N  36386  2llnneN  36544  cvrexchlem  36554  pmod2iN  36984  polcon2N  37054  paddatclN  37084  osumcllem3N  37093  ltrnval1  37269  cdleme48fv  37634  cdlemg33b  37842  trlcolem  37861  cdlemh  37952  cdlemi1  37953  cdlemi2  37954  cdlemi  37955  cdlemk4  37969  cdlemk19u1  38104  cdlemn3  38332  hgmapfval  39021  pell14qrgap  39470  stoweidlem22  42306  stoweidlem26  42310  sigarexp  43115  lindszr  44523