MPE Home 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 483 . 2 ((𝜓𝜑) → 𝜒)
3 sylanl2.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3syldanl 603 1 (((𝜓𝜑) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  mpanlr1  705  adantlrl  719  adantlrr  720  1stconst  8021  2ndconst  8022  oesuclem  8439  oelim  8448  undom  8937  mulsub  11532  divsubdiv  11805  lcmneg  16415  vdwlem12  16800  dpjidcl  19772  mplbas2  21371  monmat2matmon  22101  bwth  22689  cnextfun  23343  elbl4  23847  metucn  23855  dvradcnv  25708  dchrisum0lem2a  26793  axcontlem4  27721  cnlnadjlem2  30815  chirredlem2  31138  mdsymlem5  31154  sibfof  32720  relowlssretop  35765  matunitlindflem1  36005  poimirlem29  36038  unichnidl  36421  dmncan2  36467  cvrexchlem  37813  jm2.26  41228  radcnvrat  42395  binomcxplemnotnn0  42437  suplesup  43368  dvnmptdivc  43970  fourierdlem64  44202  fourierdlem74  44212  fourierdlem75  44213  fourierdlem83  44221  etransclem35  44301  iundjiun  44492  hoidmvlelem2  44628
  Copyright terms: Public domain W3C validator