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

Theorem orbi12d 690
 Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bi12d.1 (φ → (ψχ))
bi12d.2 (φ → (θτ))
Assertion
Ref Expression
orbi12d (φ → ((ψ θ) ↔ (χ τ)))

Proof of Theorem orbi12d
StepHypRef Expression
1 bi12d.1 . . 3 (φ → (ψχ))
21orbi1d 683 . 2 (φ → ((ψ θ) ↔ (χ θ)))
3 bi12d.2 . . 3 (φ → (θτ))
43orbi2d 682 . 2 (φ → ((χ θ) ↔ (χ τ)))
52, 4bitrd 244 1 (φ → ((ψ θ) ↔ (χ τ)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∨ wo 357 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  df-or 359 This theorem is referenced by:  pm4.39  841  3orbi123d  1251  cadbi123d  1383  eueq3  3011  sbcor  3090  sbcorg  3091  elprg  3750  eltpg  3769  preq12bg  4128  nnc0suc  4412  nndisjeq  4429  lefinlteq  4463  evenodddisjlem1  4515  fununi  5160  funcnvuni  5161  fun11iun  5305  unpreima  5408  clos1basesuc  5882  clos1basesucg  5884  connexrd  5930  connexd  5931  qsdisj  5995  ncdisjeq  6148  nc0le1  6216  leconnnc  6218  muc0or  6252  nchoicelem9  6297  nchoicelem16  6304  nchoicelem17  6305  nchoice  6308
 Copyright terms: Public domain W3C validator