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

Theorem syld3an2 1412
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 1137 . 2 ((𝜑𝜒𝜃) → 𝜑)
2 syld3an2.1 . 2 ((𝜑𝜒𝜃) → 𝜓)
3 simp3 1139 . 2 ((𝜑𝜒𝜃) → 𝜃)
4 syld3an2.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1372 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 210  df-an 400  df-3an 1090
This theorem is referenced by:  enfii  8784  nppcan2  10995  nnncan  10999  nnncan2  11001  subdivcomb2  11414  ltdivmul  11593  ledivmul  11594  ltdiv23  11609  lediv23  11610  xrmaxlt  12657  xrltmin  12658  xrmaxle  12659  xrlemin  12660  pfxtrcfv  14144  pfxco  14289  dvdssub2  15746  dvdsgcdb  15989  lcmdvdsb  16054  vdwapun  16410  poslubdg  17875  ipodrsfi  17889  mulginvcom  18370  matinvgcell  21186  mdetrsca2  21355  mdetrlin2  21358  mdetunilem5  21367  decpmatmul  21523  islp3  21897  bddibl  24592  nvpi  28602  nvabs  28607  nmmulg  31488  lineid  34023  oplecon1b  36838  opltcon1b  36842  oldmm2  36855  oldmj2  36859  cmt3N  36888  2llnneN  37046  cvrexchlem  37056  pmod2iN  37486  polcon2N  37556  paddatclN  37586  osumcllem3N  37595  ltrnval1  37771  cdleme48fv  38136  cdlemg33b  38344  trlcolem  38363  cdlemh  38454  cdlemi1  38455  cdlemi2  38456  cdlemi  38457  cdlemk4  38471  cdlemk19u1  38606  cdlemn3  38834  hgmapfval  39523  pell14qrgap  40269  mnringmulrcld  41388  stoweidlem22  43105  stoweidlem26  43109  sigarexp  43914  lindszr  45344  fv2arycl  45528
  Copyright terms: Public domain W3C validator