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

Theorem orbi2d 682
 Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
bid.1 (φ → (ψχ))
Assertion
Ref Expression
orbi2d (φ → ((θ ψ) ↔ (θ χ)))

Proof of Theorem orbi2d
StepHypRef Expression
1 bid.1 . . 3 (φ → (ψχ))
21imbi2d 307 . 2 (φ → ((¬ θψ) ↔ (¬ θχ)))
3 df-or 359 . 2 ((θ ψ) ↔ (¬ θψ))
4 df-or 359 . 2 ((θ χ) ↔ (¬ θχ))
52, 3, 43bitr4g 279 1 (φ → ((θ ψ) ↔ (θ χ)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357 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  df-or 359 This theorem is referenced by:  orbi1d  683  orbi12d  690  cad1  1398  eueq2  3010  sbc2or  3054  rexprg  3776  rextpg  3778  clos1basesucg  5884  nc0suc  6217  nmembers1lem3  6270
 Copyright terms: Public domain W3C validator