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

Theorem sylanl2 682
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 (𝜑𝜒)
21anim2i 592 . 2 ((𝜓𝜑) → (𝜓𝜒))
3 sylanl2.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3sylan 488 1 (((𝜓𝜑) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  mpanlr1  721  adantlrl  755  adantlrr  756  oesuclem  7550  oelim  7559  mulsub  10417  divsubdiv  10685  lcmneg  15240  vdwlem12  15620  dpjidcl  18378  mplbas2  19389  monmat2matmon  20548  bwth  21123  cnextfun  21778  elbl4  22278  metucn  22286  dvradcnv  24079  dchrisum0lem2a  25106  axcontlem4  25747  cnlnadjlem2  28773  chirredlem2  29096  mdsymlem5  29112  sibfof  30180  relowlssretop  32840  matunitlindflem1  33034  poimirlem29  33067  unichnidl  33459  dmncan2  33505  cvrexchlem  34182  jm2.26  37046  radcnvrat  37992  binomcxplemnotnn0  38034  suplesup  39016  dvnmptdivc  39456  fourierdlem64  39691  fourierdlem74  39701  fourierdlem75  39702  fourierdlem83  39710  etransclem35  39790  iundjiun  39981  hoidmvlelem2  40114
  Copyright terms: Public domain W3C validator