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 206  df-an 395  df-3an 1086

This theorem is referenced by:  enfii  9220  domsdomtrfi  9236  nppcan2  11529  nnncan  11533  nnncan2  11535  subdivcomb2  11948  ltdivmul  12127  ledivmul  12128  ltdiv23  12143  lediv23  12144  xrmaxlt  13200  xrltmin  13201  xrmaxle  13202  xrlemin  13203  pfxtrcfv  14683  pfxco  14829  dvdssub2  16285  dvdsgcdb  16528  lcmdvdsb  16591  vdwapun  16950  poslubdg  18413  ipodrsfi  18538  mulginvcom  19061  matinvgcell  22357  mdetrsca2  22526  mdetrlin2  22529  mdetunilem5  22538  decpmatmul  22694  islp3  23070  bddibl  25789  nvpi  30497  nvabs  30502  nmmulg  33602  lineid  35712  oplecon1b  38705  opltcon1b  38709  oldmm2  38722  oldmj2  38726  cmt3N  38755  2llnneN  38914  cvrexchlem  38924  pmod2iN  39354  polcon2N  39424  paddatclN  39454  osumcllem3N  39463  ltrnval1  39639  cdleme48fv  40004  cdlemg33b  40212  trlcolem  40231  cdlemh  40322  cdlemi1  40323  cdlemi2  40324  cdlemi  40325  cdlemk4  40339  cdlemk19u1  40474  cdlemn3  40702  hgmapfval  41391  pell14qrgap  42326  mnringmulrcld  43696  stoweidlem22  45439  stoweidlem26  45443  sigarexp  46276  lindszr  47615  fv2arycl  47799