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

Theorem bibi1d 310
 Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imbid.1 (φ → (ψχ))
Assertion
Ref Expression
bibi1d (φ → ((ψθ) ↔ (χθ)))

Proof of Theorem bibi1d
StepHypRef Expression
1 imbid.1 . . 3 (φ → (ψχ))
21bibi2d 309 . 2 (φ → ((θψ) ↔ (θχ)))
3 bicom 191 . 2 ((ψθ) ↔ (θψ))
4 bicom 191 . 2 ((χθ) ↔ (θχ))
52, 3, 43bitr4g 279 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:  bibi12d  312  bibi1  317  biass  348  eubid  2211  axext3  2336  bm1.1  2338  eqeq1  2359  pm13.183  2979  elabgt  2982  mob  3018  sbctt  3108  sbcabel  3123  br1stg  4730  isoeq2  5483  extd  5923
 Copyright terms: Public domain W3C validator