MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syld3an2 Structured version   Visualization version   GIF version

Theorem syld3an2 1519
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
StepHypRef Expression
1 simp1 1131 . 2 ((𝜑𝜒𝜃) → 𝜑)
2 syld3an2.1 . 2 ((𝜑𝜒𝜃) → 𝜓)
3 simp3 1133 . 2 ((𝜑𝜒𝜃) → 𝜃)
4 syld3an2.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1477 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  nppcan2  10502  nnncan  10506  nnncan2  10508  ltdivmul  11088  ledivmul  11089  ltdiv23  11104  lediv23  11105  xrmaxlt  12203  xrltmin  12204  xrmaxle  12205  xrlemin  12206  swrdtrcfv  13639  dvdssub2  15223  dvdsgcdb  15462  lcmdvdsb  15526  vdwapun  15878  poslubdg  17348  ipodrsfi  17362  mulginvcom  17764  matinvgcell  20441  mdetrsca2  20610  mdetrlin2  20613  mdetunilem5  20622  decpmatmul  20777  islp3  21150  bddibl  23803  nvpi  27829  nvabs  27834  nmmulg  30319  subdivcomb2  31917  lineid  32494  oplecon1b  34989  opltcon1b  34993  oldmm2  35006  oldmj2  35010  cmt3N  35039  2llnneN  35196  cvrexchlem  35206  pmod2iN  35636  polcon2N  35706  paddatclN  35736  osumcllem3N  35745  ltrnval1  35921  cdleme48fv  36287  cdlemg33b  36495  trlcolem  36514  cdlemh  36605  cdlemi1  36606  cdlemi2  36607  cdlemi  36608  cdlemk4  36622  cdlemk19u1  36757  cdlemn3  36986  hgmapfval  37678  pell14qrgap  37939  stoweidlem22  40740  stoweidlem26  40744  sigarexp  41552  pfxtrcfv  41909  pfxco  41946  lindszr  42766
  Copyright terms: Public domain W3C validator