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

Theorem sylanl2 680
 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 485 . 2 ((𝜓𝜑) → 𝜒)
3 sylanl2.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3syldanl 604 1 (((𝜓𝜑) ∧ 𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 This theorem is referenced by:  mpanlr1  705  adantlrl  719  adantlrr  720  1stconst  7800  2ndconst  7801  oesuclem  8160  oelim  8169  mulsub  11121  divsubdiv  11394  lcmneg  15999  vdwlem12  16383  dpjidcl  19248  mplbas2  20802  monmat2matmon  21524  bwth  22110  cnextfun  22764  elbl4  23265  metucn  23273  dvradcnv  25115  dchrisum0lem2a  26200  axcontlem4  26860  cnlnadjlem2  29950  chirredlem2  30273  mdsymlem5  30289  sibfof  31826  relowlssretop  35060  matunitlindflem1  35333  poimirlem29  35366  unichnidl  35749  dmncan2  35795  cvrexchlem  36995  jm2.26  40316  radcnvrat  41391  binomcxplemnotnn0  41433  suplesup  42339  dvnmptdivc  42946  fourierdlem64  43178  fourierdlem74  43188  fourierdlem75  43189  fourierdlem83  43197  etransclem35  43277  iundjiun  43465  hoidmvlelem2  43601
 Copyright terms: Public domain W3C validator