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

Theorem syl3an3b 1361
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 206 . 2 (𝜑𝜃)
3 syl3an3b.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl3an3 1358 1 ((𝜓𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036
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  df-3an 1038
This theorem is referenced by:  fresaunres1  6044  fvun2  6237  nnmsucr  7665  xrlttr  11933  iccdil  12268  icccntr  12270  absexpz  13995  posglbd  17090  f1omvdco3  17809  isdrngd  18712  unicld  20790  2ndcdisj2  21200  logrec  24435  cdj3lem3  29185  bnj563  30574  bnj1033  30798  stoweidlem14  39568
  Copyright terms: Public domain W3C validator