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  2163  cbvmo  2181  raleqbii  2574  rmo5  2757  cbvrmo  2764  ss2ab  3242  trint  4129  ssextss  4226  trsuc2OLD  4476  relop  4833  dmcosseq  4945  cotr  5054  issref  5055  cnvsym  5056  intasym  5057  intirr  5060  codir  5062  qfto  5063  cnvpo  5211  funcnvuni  5283  poxp  6189  porpss  6243  cp  7557  aceq2  7742  kmlem12  7783  kmlem15  7786  zfcndpow  8234  grothprim  8452  dfinfmr  9727  infmsup  9728  infmrgelb  9730  infmrlb  9731  xrinfmss2  10625  algcvgblem  12743  isprm2  12762  oduglb  14239  odulub  14241  isirred2  15479  isdomn2  16036  ntreq0  16810  ist0-3  17069  ist1-3  17073  ordthaus  17108  dfcon2  17141  mdsymlem8  22986  ballotlem2  23043  axrepprim  23455  axacprim  23460  dffr5  23516  dfso2  23517  dfpo2  23518  elpotr  23541  wfrlem5  23664  frrlem5  23689  isoriso  24623  mnlmxl2  24680  vecval1b  24862  vecval3b  24863  svli2  24895  isntr  25284  gtinf  25645  isdmn3  26110  moxfr  26163  isdomn3  26934  conss34  27056  onfrALTlem5  27590  onfrALTlem5VD  27941  bnj110  28169  bnj92  28173  bnj539  28202  bnj540  28203  a12study9  28399
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