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

Theorem syl3an3b 1406
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 216 . 2 (𝜑𝜃)
3 syl3an3b.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl3an3 1165 1 ((𝜓𝜒𝜑) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  fnunres2  6680  fresaunres1  6780  fvun2  7000  fvpr2g  7212  nnmsucr  8664  entrfil  9226  enpr2  10043  xrlttr  13183  iccdil  13531  icccntr  13533  hashgt23el  14464  absexpz  15345  nn0rppwr  16599  posglbdg  18461  f1omvdco3  19468  isdrngd  20766  isdrngdOLD  20768  unicld  23055  2ndcdisj2  23466  logrec  26807  cdj3lem3  32458  bnj563  34758  bnj1033  34984  lindsadd  37621  stoweidlem14  46034
  Copyright terms: Public domain W3C validator