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  1519  nfbii  1574  sb8mo  2236  cbvmo  2254  raleqbii  2658  rmo5  2841  cbvrmo  2848  ss2ab  3327  trint  4230  ssextss  4330  trsuc2OLD  4580  relop  4937  dmcosseq  5049  cotr  5158  issref  5159  cnvsym  5160  intasym  5161  intirr  5164  codir  5166  qfto  5167  cnvpo  5316  funcnvuni  5422  poxp  6355  porpss  6423  cp  7708  aceq2  7893  kmlem12  7934  kmlem15  7937  zfcndpow  8385  grothprim  8603  dfinfmr  9878  infmsup  9879  infmrgelb  9881  infmrlb  9882  xrinfmss2  10782  algcvgblem  12955  isprm2  12974  oduglb  14453  odulub  14455  isirred2  15693  isdomn2  16250  ntreq0  17031  ist0-3  17290  ist1-3  17294  ordthaus  17329  dfcon2  17362  mdsymlem8  23303  mo5f  23366  iuninc  23409  suppss2f  23452  iscusp2  23791  esumpfinvalf  23931  measiuns  24034  ballotlem2  24194  axrepprim  24635  axacprim  24640  dffr5  24851  dfso2  24852  dfpo2  24853  elpotr  24878  wfrlem5  25001  frrlem5  25026  dffun10  25194  itg2addnclem2  25676  gtinf  25741  isdmn3  26205  moxfr  26258  isdomn3  27029  conss34  27151  onfrALTlem5  28054  onfrALTlem5VD  28425  bnj110  28654  bnj92  28658  bnj539  28687  bnj540  28688  a12study9  29191
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