MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi12i Unicode version

Theorem imbi12i 316
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 303 . 2  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
3 imbi12i.1 . . 3  |-  ( ph  <->  ps )
43imbi1i 315 . 2  |-  ( (
ph  ->  th )  <->  ( ps  ->  th ) )
52, 4bitri 240 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  orimdi  820  rb-bijust  1504  nfbii  1559  sb8mo  2175  cbvmo  2193  raleqbii  2586  rmo5  2769  cbvrmo  2776  ss2ab  3254  trint  4144  ssextss  4243  trsuc2OLD  4493  relop  4850  dmcosseq  4962  cotr  5071  issref  5072  cnvsym  5073  intasym  5074  intirr  5077  codir  5079  qfto  5080  cnvpo  5229  funcnvuni  5333  poxp  6243  porpss  6297  cp  7577  aceq2  7762  kmlem12  7803  kmlem15  7806  zfcndpow  8254  grothprim  8472  dfinfmr  9747  infmsup  9748  infmrgelb  9750  infmrlb  9751  xrinfmss2  10645  algcvgblem  12763  isprm2  12782  oduglb  14259  odulub  14261  isirred2  15499  isdomn2  16056  ntreq0  16830  ist0-3  17089  ist1-3  17093  ordthaus  17128  dfcon2  17161  mdsymlem8  23006  ballotlem2  23063  mo5f  23159  iuninc  23174  suppss2f  23216  esumpfinvalf  23459  measiuns  23559  axrepprim  24063  axacprim  24068  dffr5  24180  dfso2  24181  dfpo2  24182  elpotr  24207  wfrlem5  24330  frrlem5  24355  dffun10  24523  itg2addnclem2  25003  isoriso  25314  mnlmxl2  25371  vecval1b  25553  vecval3b  25554  svli2  25586  isntr  25975  gtinf  26336  isdmn3  26801  moxfr  26854  isdomn3  27625  conss34  27747  onfrALTlem5  28605  onfrALTlem5VD  28976  bnj110  29205  bnj92  29209  bnj539  29238  bnj540  29239  a12study9  29742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator