New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  bitr4d GIF 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-1 5  ax-2 6  ax-3 7  ax-mp 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