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

Theorem sylanl2 681
Description: A syllogism inference. (Contributed by NM, 1-Jan-2005.)
Hypotheses
Ref Expression
sylanl2.1 (𝜑𝜒)
sylanl2.2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
Assertion
Ref Expression
sylanl2 (((𝜓𝜑) ∧ 𝜃) → 𝜏)

Proof of Theorem sylanl2
StepHypRef Expression
1 sylanl2.1 . . 3 (𝜑𝜒)
21adantl 481 . 2 ((𝜓𝜑) → 𝜒)
3 sylanl2.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3syldanl 602 1 (((𝜓𝜑) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  mpanlr1  706  adantlrl  720  adantlrr  721  1stconst  8125  2ndconst  8126  oesuclem  8563  oelim  8572  undom  9099  mulsub  11706  divsubdiv  11983  lcmneg  16640  vdwlem12  17030  dpjidcl  20078  mplbas2  22060  monmat2matmon  22830  bwth  23418  cnextfun  24072  elbl4  24576  metucn  24584  dvradcnv  26464  dchrisum0lem2a  27561  axcontlem4  28982  cnlnadjlem2  32087  chirredlem2  32410  mdsymlem5  32426  sibfof  34342  relowlssretop  37364  matunitlindflem1  37623  poimirlem29  37656  unichnidl  38038  dmncan2  38084  cvrexchlem  39421  evlsvvval  42573  jm2.26  43014  radcnvrat  44333  binomcxplemnotnn0  44375  suplesup  45350  dvnmptdivc  45953  fourierdlem64  46185  fourierdlem74  46195  fourierdlem75  46196  fourierdlem83  46204  etransclem35  46284  iundjiun  46475  hoidmvlelem2  46611
  Copyright terms: Public domain W3C validator