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

Theorem imbi12i 238
Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12i.1  |-  ( ph  <->  ps )
imbi12i.2  |-  ( ch  <->  th )
Assertion
Ref Expression
imbi12i  |-  ( (
ph  ->  ch )  <->  ( ps  ->  th ) )

Proof of Theorem imbi12i
StepHypRef Expression
1 imbi12i.2 . . 3  |-  ( ch  <->  th )
21imbi2i 225 . 2  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
3 imbi12i.1 . . 3  |-  ( ph  <->  ps )
43imbi1i 237 . 2  |-  ( (
ph  ->  th )  <->  ( ps  ->  th ) )
52, 4bitri 183 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  stdcn  842  nfbii  1466  sbi2v  1885  sbim  1946  sb8mo  2033  cbvmo  2059  necon4ddc  2412  raleqbii  2482  rmo5  2685  cbvrmo  2695  ss2ab  3215  snsssn  3748  trint  4102  ssextss  4205  ordsoexmid  4546  zfregfr  4558  tfi  4566  peano2  4579  peano5  4582  relop  4761  dmcosseq  4882  cotr  4992  issref  4993  cnvsym  4994  intasym  4995  intirr  4997  codir  4999  qfto  5000  cnvpom  5153  cnvsom  5154  funcnvuni  5267  poxp  6211  infmoti  7005  dfinfre  8872  bezoutlembi  11960  algcvgblem  12003  isprm2  12071  ntreq0  12926  ss1oel2o  14026
  Copyright terms: Public domain W3C validator