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

Theorem bibi2d 309
 Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Hypothesis
Ref Expression
imbid.1 (φ → (ψχ))
Assertion
Ref Expression
bibi2d (φ → ((θψ) ↔ (θχ)))

Proof of Theorem bibi2d
StepHypRef Expression
1 imbid.1 . . . . 5 (φ → (ψχ))
21pm5.74i 236 . . . 4 ((φψ) ↔ (φχ))
32bibi2i 304 . . 3 (((φθ) ↔ (φψ)) ↔ ((φθ) ↔ (φχ)))
4 pm5.74 235 . . 3 ((φ → (θψ)) ↔ ((φθ) ↔ (φψ)))
5 pm5.74 235 . . 3 ((φ → (θχ)) ↔ ((φθ) ↔ (φχ)))
63, 4, 53bitr4i 268 . 2 ((φ → (θψ)) ↔ (φ → (θχ)))
76pm5.74ri 237 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:  bibi1d  310  bibi12d  312  biantr  897  bimsc1  904  eujust  2206  eujustALT  2207  euf  2210  ceqex  2969  reu6i  3027  sbc2or  3054  iotaval  4350  iota5  4359  copsexg  4607  isoeq1  5482  isoeq3  5484  isores2  5493  isoini2  5498  caovord  5629  extd  5923
 Copyright terms: Public domain W3C validator