ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi12i Structured version   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  1359  sbi2v  1769  sbim  1824  sb8mo  1911  cbvmo  1937  necon4ddc  2271  raleqbii  2330  rmo5  2519  cbvrmo  2526  ss2ab  3002  snsssn  3523  trint  3860  ssextss  3947  ordsoexmid  4240  tfi  4248  peano2  4261  peano5  4264  relop  4429  dmcosseq  4546  cotr  4649  issref  4650  cnvsym  4651  intasym  4652  intirr  4654  codir  4656  qfto  4657  cnvpom  4803  cnvsom  4804  funcnvuni  4911  poxp  5794  peano5setOLD  9398
  Copyright terms: Public domain W3C validator