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

Theorem syl3an3b 1356
 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 205 . 2 (𝜑𝜃)
3 syl3an3b.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl3an3 1353 1 ((𝜓𝜒𝜑) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  fresaunres1  5990  fvun2  6180  nnmsucr  7592  xrlttr  11849  iccdil  12181  icccntr  12183  absexpz  13893  posglbd  16973  f1omvdco3  17692  isdrngd  18595  unicld  20660  2ndcdisj2  21070  logrec  24301  cdj3lem3  28681  bnj563  30067  bnj1033  30291  stoweidlem14  38907
 Copyright terms: Public domain W3C validator