MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi12i Unicode version

Theorem imbi12i 317
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 304 . 2  |-  ( (
ph  ->  ch )  <->  ( ph  ->  th ) )
3 imbi12i.1 . . 3  |-  ( ph  <->  ps )
43imbi1i 316 . 2  |-  ( (
ph  ->  th )  <->  ( ps  ->  th ) )
52, 4bitri 241 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  orimdi  821  rb-bijust  1520  nfbii  1575  sb8mo  2273  cbvmo  2291  raleqbii  2696  rmo5  2884  cbvrmo  2891  ss2ab  3371  trint  4277  ssextss  4377  relop  4982  dmcosseq  5096  cotr  5205  issref  5206  cnvsym  5207  intasym  5208  intirr  5211  codir  5213  qfto  5214  cnvpo  5369  funcnvuni  5477  poxp  6417  porpss  6485  cp  7771  aceq2  7956  kmlem12  7997  kmlem15  8000  zfcndpow  8447  grothprim  8665  dfinfmr  9941  infmsup  9942  infmrgelb  9944  infmrlb  9945  xrinfmss2  10845  algcvgblem  13023  isprm2  13042  oduglb  14521  odulub  14523  isirred2  15761  isdomn2  16314  ntreq0  17096  ist0-3  17363  ist1-3  17367  ordthaus  17402  dfcon2  17435  iscusp2  18285  mdsymlem8  23866  mo5f  23925  iuninc  23964  suppss2f  24002  tosglb  24145  esumpfinvalf  24419  axrepprim  25104  axacprim  25109  dffr5  25324  dfso2  25325  dfpo2  25326  elpotr  25351  dffun10  25667  itg2addnclem2  26156  gtinf  26212  isdmn3  26574  moxfr  26623  isdomn3  27391  conss34  27512  dff14a  27959  onfrALTlem5  28339  onfrALTlem5VD  28706  bnj110  28935  bnj92  28939  bnj539  28968  bnj540  28969
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 178
  Copyright terms: Public domain W3C validator