MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi12i Structured version   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 4    <-> wb 178
This theorem is referenced by:  orimdi  822  rb-bijust  1524  nfbii  1579  sb8mo  2302  cbvmo  2320  raleqbii  2737  rmo5  2926  cbvrmo  2933  ss2ab  3413  trint  4319  ssextss  4419  relop  5025  dmcosseq  5139  cotr  5248  issref  5249  cnvsym  5250  intasym  5251  intirr  5254  codir  5256  qfto  5257  cnvpo  5412  funcnvuni  5520  poxp  6460  porpss  6528  cp  7817  aceq2  8002  kmlem12  8043  kmlem15  8046  zfcndpow  8493  grothprim  8711  dfinfmr  9987  infmsup  9988  infmrgelb  9990  infmrlb  9991  xrinfmss2  10891  algcvgblem  13070  isprm2  13089  oduglb  14568  odulub  14570  isirred2  15808  isdomn2  16361  ntreq0  17143  ist0-3  17411  ist1-3  17415  ordthaus  17450  dfcon2  17484  iscusp2  18334  mdsymlem8  23915  mo5f  23974  iuninc  24013  suppss2f  24051  tosglb  24194  esumpfinvalf  24468  axrepprim  25153  axacprim  25158  dffr5  25378  dfso2  25379  dfpo2  25380  elpotr  25410  itg2addnclem2  26259  gtinf  26324  isdmn3  26686  moxfr  26735  isdomn3  27502  conss34  27623  dff14a  28084  onfrALTlem5  28690  onfrALTlem5VD  29059  bnj110  29291  bnj92  29295  bnj539  29324  bnj540  29325
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 179
  Copyright terms: Public domain W3C validator