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

Theorem bibi12d 224
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 222 . 2
3 imbi12d.2 . . 3
43bibi2d 221 . 2
52, 4bitrd 177 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm5.32  426  bi2bian9  540  cleqh  2134  abbi  2148  cleqf  2198  vtoclb  2605  vtoclbg  2608  ceqsexg  2666  elabgf  2679  reu6  2724  ru  2757  sbcbig  2803  sbcne12g  2862  sbcnestgf  2891  preq12bg  3535  nalset  3878  opthg  3966  opelopabsb  3988  opeliunxp2  4419  resieq  4565  elimasng  4636  cbviota  4815  iota2df  4834  fnbrfvb  5157  fvelimab  5172  fmptco  5273  fsng  5279  fressnfv  5293  funfvima3  5335  isorel  5391  isocnv  5394  isocnv2  5395  isotr  5399  ovg  5581  caovcang  5604  caovordg  5610  caovord3d  5613  caovord  5614  dftpos4  5819  ecopovsym  6138  ecopovsymg  6141  ltanqg  6384  ltmnqg  6385  elinp  6457  prnmaxl  6471  prnminu  6472  ltasrg  6698  axpre-ltadd  6770  zextle  8107  zextlt  8108  bj-nalset  9348  bj-d0clsepcl  9382  bj-nn0sucALT  9432
  Copyright terms: Public domain W3C validator