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

Theorem imbi12i 239
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 226 . 2  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
3 imbi12i.1 . . 3  |-  ( ph  <->  ps )
43imbi1i 238 . 2  |-  ( (
ph  ->  th )  <->  ( ps  ->  th ) )
52, 4bitri 184 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  stdcn  847  nfbii  1473  sbi2v  1892  sbim  1953  sb8mo  2040  cbvmo  2066  necon4ddc  2419  raleqbii  2489  rmo5  2693  cbvrmo  2704  ss2ab  3225  snsssn  3763  trint  4118  ssextss  4222  ordsoexmid  4563  zfregfr  4575  tfi  4583  peano2  4596  peano5  4599  relop  4779  dmcosseq  4900  cotr  5012  issref  5013  cnvsym  5014  intasym  5015  intirr  5017  codir  5019  qfto  5020  cnvpom  5173  cnvsom  5174  funcnvuni  5287  poxp  6235  infmoti  7029  dfinfre  8915  bezoutlembi  12008  algcvgblem  12051  isprm2  12119  ntreq0  13671  ss1oel2o  14782
  Copyright terms: Public domain W3C validator