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  822  rb-bijust  1505  nfbii  1557  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  5282  poxp  6188  porpss  6242  cp  7556  aceq2  7741  kmlem12  7782  kmlem15  7785  zfcndpow  8233  grothprim  8451  dfinfmr  9726  infmsup  9727  infmrgelb  9729  infmrlb  9730  xrinfmss2  10623  algcvgblem  12741  isprm2  12760  oduglb  14237  odulub  14239  isirred2  15477  isdomn2  16034  ntreq0  16808  ist0-3  17067  ist1-3  17071  ordthaus  17106  dfcon2  17139  mdsymlem8  22982  ballotlem2  23040  axrepprim  23452  axacprim  23457  dffr5  23513  dfso2  23514  dfpo2  23515  elpotr  23538  wfrlem5  23661  frrlem5  23686  isoriso  24611  mnlmxl2  24668  vecval1b  24850  vecval3b  24851  svli2  24883  isntr  25272  gtinf  25633  isdmn3  26098  moxfr  26151  isdomn3  26922  conss34  27044  onfrALTlem5  27578  onfrALTlem5VD  27929  bnj110  28157  bnj92  28161  bnj539  28190  bnj540  28191  a12study9  28387
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