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  815  nfbii  1432  sbi2v  1846  sbim  1902  sb8mo  1989  cbvmo  2015  necon4ddc  2355  raleqbii  2422  rmo5  2621  cbvrmo  2628  ss2ab  3133  snsssn  3656  trint  4009  ssextss  4110  ordsoexmid  4445  zfregfr  4456  tfi  4464  peano2  4477  peano5  4480  relop  4657  dmcosseq  4778  cotr  4888  issref  4889  cnvsym  4890  intasym  4891  intirr  4893  codir  4895  qfto  4896  cnvpom  5049  cnvsom  5050  funcnvuni  5160  poxp  6095  infmoti  6881  dfinfre  8671  bezoutlembi  11589  algcvgblem  11626  isprm2  11694  ntreq0  12196  ss1oel2o  12991
  Copyright terms: Public domain W3C validator