Theorem syld3an2 1429

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

Syntax hints:   → wi 4   ∧ w3a 1097

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

This theorem is referenced by:  enfii  9148  domsdomtrfi  9164  nppcan2  11456  nnncan  11460  nnncan2  11462  div11  11867  subdivcomb2  11881  ltdivmul  12061  ledivmul  12062  ltdiv23  12077  lediv23  12078  xrmaxlt  13178  xrltmin  13179  xrmaxle  13180  xrlemin  13181  pfxtrcfv  14700  pfxco  14845  dvdssub2  16326  dvdsgcdb  16570  lcmdvdsb  16638  vdwapun  17001  poslubdg  18435  ipodrsfi  18562  mulginvcom  19132  matinvgcell  22483  mdetrsca2  22652  mdetrlin2  22655  mdetunilem5  22664  decpmatmul  22820  islp3  23194  bddibl  25890  nvpi  30827  nvabs  30832  nmmulg  34224  fineqvnttrclselem2  35379  fineqvnttrclselem3  35380  lineid  36394  oplecon1b  39786  opltcon1b  39790  oldmm2  39803  oldmj2  39807  cmt3N  39836  2llnneN  39994  cvrexchlem  40004  pmod2iN  40434  polcon2N  40504  paddatclN  40534  osumcllem3N  40543  ltrnval1  40719  cdleme48fv  41084  cdlemg33b  41292  trlcolem  41311  cdlemh  41402  cdlemi1  41403  cdlemi2  41404  cdlemi  41405  cdlemk4  41419  cdlemk19u1  41554  cdlemn3  41782  hgmapfval  42471  pell14qrgap  43413  mnringmulrcld  44765  stoweidlem22  46557  stoweidlem26  46561  sigarexp  47394  lindszr  49052  fv2arycl  49231