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

Theorem bitr3d 246
Description: Deduction form of bitr3i 242. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3d.1 (φ → (ψχ))
bitr3d.2 (φ → (ψθ))
Assertion
Ref Expression
bitr3d (φ → (χθ))

Proof of Theorem bitr3d
StepHypRef Expression
1 bitr3d.1 . . 3 (φ → (ψχ))
21bicomd 192 . 2 (φ → (χψ))
3 bitr3d.2 . 2 (φ → (ψθ))
42, 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:  3bitrrd  271  3bitr3d  274  3bitr3rd  275  biass  348  sbequ12a  1921  sbco2  2086  sbco3  2088  sbcom  2089  sb9i  2094  sbcom2  2114  sbal1  2126  sbal  2127  csbiebt  3172  opkelimagekg  4271  copsex2t  4608  copsex2g  4609  resieq  4979  fnssresb  5195  funimass5  5405  isocnv  5491  isoini  5497  ovmpt2x  5712  brcupg  5814  brcomposeg  5819  brcrossg  5848  enpw1  6062  enmap1lem3  6071  nenpw1pwlem2  6085  te0c  6237
  Copyright terms: Public domain W3C validator