Theorem syld3an2 1438

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  enfii  9180  domsdomtrfi  9196  nppcan2  11513  nnncan  11517  nnncan2  11519  div11  11924  subdivcomb2  11935  ltdivmul  12114  ledivmul  12115  ltdiv23  12130  lediv23  12131  xrmaxlt  13233  xrltmin  13234  xrmaxle  13235  xrlemin  13236  pfxtrcfv  14762  pfxco  14909  dvdssub2  16391  dvdsgcdb  16635  lcmdvdsb  16703  vdwapun  17066  poslubdg  18500  ipodrsfi  18627  mulginvcom  19222  matinvgcell  22657  mdetrsca2  22826  mdetrlin2  22829  mdetunilem5  22838  decpmatmul  22997  islp3  23371  bddibl  26067  nvpi  31148  nvabs  31153  nmmulg  34476  fineqvnttrclselem2  35648  fineqvnttrclselem3  35649  lineid  36663  oplecon1b  40074  opltcon1b  40078  oldmm2  40091  oldmj2  40095  cmt3N  40124  2llnneN  40282  cvrexchlem  40292  pmod2iN  40722  polcon2N  40792  paddatclN  40822  osumcllem3N  40831  ltrnval1  41007  cdleme48fv  41372  cdlemg33b  41580  trlcolem  41599  cdlemh  41690  cdlemi1  41691  cdlemi2  41692  cdlemi  41693  cdlemk4  41707  cdlemk19u1  41842  cdlemn3  42070  hgmapfval  42759  pell14qrgap  43716  mnringmulrcld  45066  stoweidlem22  46850  stoweidlem26  46854  sigarexp  47687  lindszr  49399  fv2arycl  49578