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

Theorem imbi12i 237
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 224 . 2  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
3 imbi12i.1 . . 3  |-  ( ph  <->  ps )
43imbi1i 236 . 2  |-  ( (
ph  ->  th )  <->  ( ps  ->  th ) )
52, 4bitri 182 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  nfbii  1405  sbi2v  1817  sbim  1872  sb8mo  1959  cbvmo  1985  necon4ddc  2323  raleqbii  2386  rmo5  2578  cbvrmo  2585  ss2ab  3078  snsssn  3590  trint  3928  ssextss  4023  ordsoexmid  4353  zfregfr  4364  tfi  4372  peano2  4385  peano5  4388  relop  4556  dmcosseq  4674  cotr  4782  issref  4783  cnvsym  4784  intasym  4785  intirr  4787  codir  4789  qfto  4790  cnvpom  4941  cnvsom  4942  funcnvuni  5050  poxp  5956  infmoti  6670  dfinfre  8355  bezoutlembi  10900  algcvgblem  10937  isprm2  11005  ss1oel2o  11357
  Copyright terms: Public domain W3C validator