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  833  nfbii  1453  sbi2v  1872  sbim  1933  sb8mo  2020  cbvmo  2046  necon4ddc  2399  raleqbii  2469  rmo5  2672  cbvrmo  2679  ss2ab  3196  snsssn  3724  trint  4077  ssextss  4180  ordsoexmid  4521  zfregfr  4533  tfi  4541  peano2  4554  peano5  4557  relop  4736  dmcosseq  4857  cotr  4967  issref  4968  cnvsym  4969  intasym  4970  intirr  4972  codir  4974  qfto  4975  cnvpom  5128  cnvsom  5129  funcnvuni  5239  poxp  6179  infmoti  6972  dfinfre  8827  bezoutlembi  11888  algcvgblem  11925  isprm2  11993  ntreq0  12532  ss1oel2o  13565
  Copyright terms: Public domain W3C validator