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

Theorem imbi12i 326
Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-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.1 . 2  |-  ( ph  <->  ps )
2 imbi12i.2 . 2  |-  ( ch  <->  th )
3 imbi12 322 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
41, 2, 3mp2 9 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  th ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  orimdi  843  rb-bijust  1556  nfbii  1614  sbnf2  2144  sb8mo  2295  cbvmo  2297  raleqbii  2766  rmo5  2960  cbvrmo  2967  ss2ab  3441  sbcssg  3811  trint  4421  ssextss  4567  relop  5011  dmcosseq  5122  cotr  5231  issref  5232  cnvsym  5233  intasym  5234  intirr  5237  codir  5239  qfto  5240  cnvpo  5396  porpss  6385  funcnvuni  6551  poxp  6705  cp  8119  aceq2  8310  kmlem12  8351  kmlem15  8354  zfcndpow  8804  grothprim  9022  dfinfmr  10328  infmsup  10329  infmrgelb  10331  infmrlb  10332  xrinfmss2  11294  algcvgblem  13773  isprm2  13792  oduglb  15330  odulub  15332  isirred2  16815  isdomn2  17393  ntreq0  18703  ist0-3  18971  ist1-3  18975  ordthaus  19010  dfcon2  19045  iscusp2  19899  mdsymlem8  25836  mo5f  25890  iuninc  25933  suppss2f  25976  oduprs  26139  tosglblem  26152  esumpfinvalf  26547  axrepprim  27375  axacprim  27380  dffr5  27585  dfso2  27586  dfpo2  27587  elpotr  27616  itg2addnclem2  28470  gtinf  28540  isdmn3  28900  sbcimi  28941  moxfr  29054  isdomn3  29598  conss34  29724  dff14a  30170  onfrALTlem5  31346  onfrALTlem5VD  31717  bnj110  31947  bnj92  31951  bnj539  31980  bnj540  31981
  Copyright terms: Public domain W3C validator