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  823  rb-bijust  1509  nfbii  1561  sb8mo  2137  cbvmo  2155  raleqbii  2548  rmo5  2731  cbvrmo  2738  ss2ab  3216  trint  4102  ssextss  4199  trsuc2OLD  4449  relop  4822  dmcosseq  4934  cotr  5043  issref  5044  cnvsym  5045  intasym  5046  intirr  5049  codir  5051  qfto  5052  cnvpo  5200  funcnvuni  5255  poxp  6161  porpss  6215  cp  7529  aceq2  7714  kmlem12  7755  kmlem15  7758  zfcndpow  8206  grothprim  8424  dfinfmr  9699  infmsup  9700  infmrgelb  9702  infmrlb  9703  xrinfmss2  10596  algcvgblem  12710  isprm2  12729  oduglb  14206  odulub  14208  isirred2  15446  isdomn2  16003  ntreq0  16777  ist0-3  17036  ist1-3  17040  ordthaus  17075  dfcon2  17108  mdsymlem8  22951  ballotlem2  23009  axrepprim  23421  axacprim  23426  dffr5  23482  dfso2  23483  dfpo2  23484  elpotr  23507  wfrlem5  23630  frrlem5  23655  isoriso  24580  mnlmxl2  24637  vecval1b  24819  vecval3b  24820  svli2  24852  isntr  25241  gtinf  25602  isdmn3  26067  moxfr  26120  isdomn3  26891  conss34  27014  onfrALTlem5  27443  onfrALTlem5VD  27794  bnj110  28022  bnj92  28026  bnj539  28055  bnj540  28056  a12study9  28370
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