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

Theorem imbi12i 318
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 305 . 2  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
3 imbi12i.1 . . 3  |-  ( ph  <->  ps )
43imbi1i 317 . 2  |-  ( (
ph  ->  th )  <->  ( ps  ->  th ) )
52, 4bitri 242 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  orimdi  823  rb-bijust  1509  nfbii  1561  cbvmo  2153  raleqbii  2546  rmo5  2726  cbvrmo  2733  ss2ab  3202  trint  4088  ssextss  4185  trsuc2OLD  4435  relop  4808  dmcosseq  4920  cotr  5029  issref  5030  cnvsym  5031  intasym  5032  intirr  5035  codir  5037  qfto  5038  cnvpo  5186  funcnvuni  5241  poxp  6147  porpss  6201  cp  7515  aceq2  7700  kmlem12  7741  kmlem15  7744  zfcndpow  8192  grothprim  8410  dfinfmr  9685  infmsup  9686  infmrgelb  9688  infmrlb  9689  xrinfmss2  10581  algcvgblem  12695  isprm2  12714  oduglb  14191  odulub  14193  isirred2  15431  isdomn2  15988  ntreq0  16762  ist0-3  17021  ist1-3  17025  ordthaus  17060  dfcon2  17093  mdsymlem8  22936  ballotlem2  22994  axrepprim  23406  axacprim  23411  dffr5  23467  dfso2  23468  dfpo2  23469  elpotr  23492  wfrlem5  23615  frrlem5  23640  isoriso  24565  mnlmxl2  24622  vecval1b  24804  vecval3b  24805  svli2  24837  isntr  25226  gtinf  25587  isdmn3  26052  moxfr  26105  isdomn3  26876  conss34  26999  onfrALTlem5  27344  onfrALTlem5VD  27695  bnj110  27923  bnj92  27927  bnj539  27956  bnj540  27957  a12study9  28271
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator