Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  bibi12d GIF version

Theorem bibi12d 228
 Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1 (𝜑 → (𝜓𝜒))
imbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
bibi12d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))

Proof of Theorem bibi12d
StepHypRef Expression
1 imbi12d.1 . . 3 (𝜑 → (𝜓𝜒))
21bibi1d 226 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43bibi2d 225 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 181 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  pm5.32  434  bi2bian9  550  cleqh  2153  abbi  2167  cleqf  2217  vtoclb  2628  vtoclbg  2631  ceqsexg  2695  elabgf  2708  reu6  2753  ru  2786  sbcbig  2832  sbcne12g  2896  sbcnestgf  2925  preq12bg  3572  nalset  3915  opthg  4003  opelopabsb  4025  wetriext  4329  opeliunxp2  4504  resieq  4650  elimasng  4721  cbviota  4900  iota2df  4919  fnbrfvb  5242  fvelimab  5257  fmptco  5358  fsng  5364  fressnfv  5378  funfvima3  5420  isorel  5476  isocnv  5479  isocnv2  5480  isotr  5484  ovg  5667  caovcang  5690  caovordg  5696  caovord3d  5699  caovord  5700  dftpos4  5909  ecopovsym  6233  ecopovsymg  6236  nneneq  6351  supmoti  6399  supsnti  6409  isotilem  6410  isoti  6411  ltanqg  6556  ltmnqg  6557  elinp  6630  prnmaxl  6644  prnminu  6645  ltasrg  6913  axpre-ltadd  7018  zextle  8389  zextlt  8390  rexfiuz  9816  climshft  10056  dvdsext  10167  ltoddhalfle  10205  halfleoddlt  10206  bj-nalset  10402  bj-d0clsepcl  10436  bj-nn0sucALT  10490
 Copyright terms: Public domain W3C validator