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  2150  ss2ab  3162  trint  4025  ssextss  4121  trsuc2OLD  4370  relop  4741  dmcosseq  4853  cotr  4962  issref  4963  cnvsym  4964  intasym  4965  intirr  4968  codir  4970  qfto  4971  cnvpo  5119  funcnvuni  5174  poxp  6079  porpss  6133  cp  7445  aceq2  7630  kmlem12  7671  kmlem15  7674  zfcndpow  8118  grothprim  8336  dfinfmr  9611  infmsup  9612  infmrgelb  9614  infmrlb  9615  xrinfmss2  10507  algcvgblem  12621  isprm2  12640  oduglb  14087  odulub  14089  isirred2  15318  isdomn2  15872  ntreq0  16646  ist0-3  16905  ist1-3  16909  ordthaus  16944  dfcon2  16977  mdsymlem8  22820  axrepprim  23219  axacprim  23224  dffr5  23280  dfso2  23281  dfpo2  23282  elpotr  23305  wfrlem5  23428  frrlem5  23453  isoriso  24378  mnlmxl2  24435  vecval1b  24617  vecval3b  24618  svli2  24650  isntr  25039  gtinf  25400  isdmn3  25865  moxfr  25918  isdomn3  26689  conss34  26812  onfrALTlem5  27097  onfrALTlem5VD  27448  bnj110  27676  bnj92  27680  bnj539  27709  bnj540  27710  a12study9  28024
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