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  817  nfbii  1434  sbi2v  1848  sbim  1904  sb8mo  1991  cbvmo  2017  necon4ddc  2357  raleqbii  2424  rmo5  2623  cbvrmo  2630  ss2ab  3135  snsssn  3658  trint  4011  ssextss  4112  ordsoexmid  4447  zfregfr  4458  tfi  4466  peano2  4479  peano5  4482  relop  4659  dmcosseq  4780  cotr  4890  issref  4891  cnvsym  4892  intasym  4893  intirr  4895  codir  4897  qfto  4898  cnvpom  5051  cnvsom  5052  funcnvuni  5162  poxp  6097  infmoti  6883  dfinfre  8682  bezoutlembi  11620  algcvgblem  11657  isprm2  11725  ntreq0  12228  ss1oel2o  13116
  Copyright terms: Public domain W3C validator