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  848  nfbii  1484  sbi2v  1904  sbim  1965  sb8mo  2052  cbvmo  2078  necon4ddc  2432  raleqbii  2502  rmo5  2706  cbvrmo  2717  ss2ab  3238  snsssn  3776  trint  4131  ssextss  4238  ordsoexmid  4579  zfregfr  4591  tfi  4599  peano2  4612  peano5  4615  relop  4795  dmcosseq  4916  cotr  5028  issref  5029  cnvsym  5030  intasym  5031  intirr  5033  codir  5035  qfto  5036  cnvpom  5189  cnvsom  5190  funcnvuni  5304  poxp  6257  infmoti  7057  dfinfre  8943  bezoutlembi  12038  algcvgblem  12081  isprm2  12149  ntreq0  14089  ss1oel2o  15202
  Copyright terms: Public domain W3C validator