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  1556  sb8mo  2162  cbvmo  2180  raleqbii  2573  rmo5  2756  cbvrmo  2763  ss2ab  3241  trint  4128  ssextss  4227  trsuc2OLD  4477  relop  4834  dmcosseq  4946  cotr  5055  issref  5056  cnvsym  5057  intasym  5058  intirr  5061  codir  5063  qfto  5064  cnvpo  5213  funcnvuni  5317  poxp  6227  porpss  6281  cp  7561  aceq2  7746  kmlem12  7787  kmlem15  7790  zfcndpow  8238  grothprim  8456  dfinfmr  9731  infmsup  9732  infmrgelb  9734  infmrlb  9735  xrinfmss2  10629  algcvgblem  12747  isprm2  12766  oduglb  14243  odulub  14245  isirred2  15483  isdomn2  16040  ntreq0  16814  ist0-3  17073  ist1-3  17077  ordthaus  17112  dfcon2  17145  mdsymlem8  22990  ballotlem2  23047  mo5f  23143  iuninc  23158  suppss2f  23201  esumpfinvalf  23444  measiuns  23544  axrepprim  24048  axacprim  24053  dffr5  24110  dfso2  24111  dfpo2  24112  elpotr  24137  wfrlem5  24260  frrlem5  24285  dffun10  24453  isoriso  25212  mnlmxl2  25269  vecval1b  25451  vecval3b  25452  svli2  25484  isntr  25873  gtinf  26234  isdmn3  26699  moxfr  26752  isdomn3  27523  conss34  27645  onfrALTlem5  28307  onfrALTlem5VD  28661  bnj110  28890  bnj92  28894  bnj539  28923  bnj540  28924  a12study9  29120
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