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

Theorem sylanl2 677
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 482 . 2 ((𝜓𝜑) → 𝜒)
3 sylanl2.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3syldanl 601 1 (((𝜓𝜑) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  mpanlr1  702  adantlrl  716  adantlrr  717  1stconst  7786  2ndconst  7787  oesuclem  8141  oelim  8150  mulsub  11072  divsubdiv  11345  lcmneg  15937  vdwlem12  16318  dpjidcl  19100  mplbas2  20169  monmat2matmon  21348  bwth  21934  cnextfun  22588  elbl4  23088  metucn  23096  dvradcnv  24924  dchrisum0lem2a  26007  axcontlem4  26667  cnlnadjlem2  29759  chirredlem2  30082  mdsymlem5  30098  sibfof  31484  relowlssretop  34513  matunitlindflem1  34755  poimirlem29  34788  unichnidl  35177  dmncan2  35223  cvrexchlem  36422  jm2.26  39464  radcnvrat  40511  binomcxplemnotnn0  40553  suplesup  41472  dvnmptdivc  42088  fourierdlem64  42321  fourierdlem74  42331  fourierdlem75  42332  fourierdlem83  42340  etransclem35  42420  iundjiun  42608  hoidmvlelem2  42744
  Copyright terms: Public domain W3C validator