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  1558  sb8mo  2164  cbvmo  2182  raleqbii  2575  rmo5  2758  cbvrmo  2765  ss2ab  3243  trint  4130  ssextss  4229  trsuc2OLD  4479  relop  4836  dmcosseq  4948  cotr  5057  issref  5058  cnvsym  5059  intasym  5060  intirr  5063  codir  5065  qfto  5066  cnvpo  5215  funcnvuni  5319  poxp  6229  porpss  6283  cp  7563  aceq2  7748  kmlem12  7789  kmlem15  7792  zfcndpow  8240  grothprim  8458  dfinfmr  9733  infmsup  9734  infmrgelb  9736  infmrlb  9737  xrinfmss2  10631  algcvgblem  12749  isprm2  12768  oduglb  14245  odulub  14247  isirred2  15485  isdomn2  16042  ntreq0  16816  ist0-3  17075  ist1-3  17079  ordthaus  17114  dfcon2  17147  mdsymlem8  22992  ballotlem2  23049  mo5f  23145  iuninc  23160  suppss2f  23203  esumpfinvalf  23446  measiuns  23546  axrepprim  24050  axacprim  24055  dffr5  24112  dfso2  24113  dfpo2  24114  elpotr  24139  wfrlem5  24262  frrlem5  24287  dffun10  24455  itg2addnclem2  24934  isoriso  25223  mnlmxl2  25280  vecval1b  25462  vecval3b  25463  svli2  25495  isntr  25884  gtinf  26245  isdmn3  26710  moxfr  26763  isdomn3  27534  conss34  27656  onfrALTlem5  28363  onfrALTlem5VD  28734  bnj110  28963  bnj92  28967  bnj539  28996  bnj540  28997  a12study9  29193
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