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

Theorem syl3an3b 1402
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 215 . 2 (𝜑𝜃)
3 syl3an3b.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl3an3 1162 1 ((𝜓𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1084
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 395  df-3an 1086
This theorem is referenced by:  fnunres2  6668  fresaunres1  6770  fvun2  6989  fvpr2g  7200  nnmsucr  8646  entrfil  9213  enpr2  10027  xrlttr  13154  iccdil  13502  icccntr  13504  hashgt23el  14419  absexpz  15288  posglbdg  18410  f1omvdco3  19416  isdrngd  20669  isdrngdOLD  20671  unicld  22994  2ndcdisj2  23405  logrec  26740  cdj3lem3  32320  bnj563  34505  bnj1033  34731  lindsadd  37217  nn0rppwr  42028  stoweidlem14  45540
  Copyright terms: Public domain W3C validator