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

Theorem imbi12i 228
 Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12i.1
imbi12i.2
Assertion
Ref Expression
imbi12i

Proof of Theorem imbi12i
StepHypRef Expression
1 imbi12i.2 . . 3
21imbi2i 215 . 2
3 imbi12i.1 . . 3
43imbi1i 227 . 2
52, 4bitri 173 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:  nfbii  1362  sbi2v  1772  sbim  1827  sb8mo  1914  cbvmo  1940  necon4ddc  2277  raleqbii  2336  rmo5  2525  cbvrmo  2532  ss2ab  3008  snsssn  3532  trint  3869  ssextss  3956  ordsoexmid  4286  zfregfr  4298  tfi  4305  peano2  4318  peano5  4321  relop  4486  dmcosseq  4603  cotr  4706  issref  4707  cnvsym  4708  intasym  4709  intirr  4711  codir  4713  qfto  4714  cnvpom  4860  cnvsom  4861  funcnvuni  4968  poxp  5853  algcvgblem  9888  peano5setOLD  10065
 Copyright terms: Public domain W3C validator