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

Theorem bitr4d 247
Description: Deduction form of bitr4i 243. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr4d.1
bitr4d.2
Assertion
Ref Expression
bitr4d

Proof of Theorem bitr4d
StepHypRef Expression
1 bitr4d.1 . 2
2 bitr4d.2 . . 3
32bicomd 192 . 2
41, 3bitrd 244 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176
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 177
This theorem is referenced by:  3bitr2d  272  3bitr2rd  273  3bitr4d  276  3bitr4rd  277  bianabs  850  3anibar  1123  iota1  4353  lefinlteq  4463  funbrfv2b  5362  dffn5  5363  fnrnfv  5364  fniniseg  5371  dff13  5471  isoini  5497  caovord3  5631  ce0ncpw1  6185  cantcb  6335
  Copyright terms: Public domain W3C validator