NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl7 Unicode version

Theorem syl7 63
Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
Hypotheses
Ref Expression
syl7.1
syl7.2
Assertion
Ref Expression
syl7

Proof of Theorem syl7
StepHypRef Expression
1 syl7.1 . . 3
21a1i 10 . 2
3 syl7.2 . 2
42, 3syl5d 62 1
Colors of variables: wff setvar class
Syntax hints:   wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl7bi  221  syl3an3  1217  ax10lem4  1941  hbae  1953  hbae-o  2153  ax11  2155  sfinltfin  4535
  Copyright terms: Public domain W3C validator