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

Theorem syl3an3b 1530
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3b.1 (𝜑𝜃)
syl3an3b.2 ((𝜓𝜒𝜃) → 𝜏)
Assertion
Ref Expression
syl3an3b ((𝜓𝜒𝜑) → 𝜏)

Proof of Theorem syl3an3b
StepHypRef Expression
1 syl3an3b.1 . . 3 (𝜑𝜃)
21biimpi 208 . 2 (𝜑𝜃)
3 syl3an3b.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl3an3 1211 1 ((𝜓𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  w3a 1113
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 199  df-an 387  df-3an 1115
This theorem is referenced by:  fresaunres1  6314  fvun2  6517  nnmsucr  7972  xrlttr  12259  iccdil  12603  icccntr  12605  absexpz  14422  posglbd  17503  f1omvdco3  18219  isdrngd  19128  unicld  21221  2ndcdisj2  21631  logrec  24903  cdj3lem3  29852  bnj563  31359  bnj1033  31583  lindsadd  33946  stoweidlem14  41025
  Copyright terms: Public domain W3C validator