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  1403  sbi2v  1814  sbim  1869  sb8mo  1956  cbvmo  1982  necon4ddc  2318  raleqbii  2379  rmo5  2570  cbvrmo  2577  ss2ab  3063  snsssn  3561  trint  3898  ssextss  3983  ordsoexmid  4313  zfregfr  4324  tfi  4331  peano2  4344  peano5  4347  relop  4514  dmcosseq  4631  cotr  4736  issref  4737  cnvsym  4738  intasym  4739  intirr  4741  codir  4743  qfto  4744  cnvpom  4890  cnvsom  4891  funcnvuni  4999  poxp  5884  infmoti  6500  dfinfre  8101  bezoutlembi  10538  algcvgblem  10575  isprm2  10643
  Copyright terms: Public domain W3C validator