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

Theorem imbi12i 324
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 320 . 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  845  nanbi  1350  nanbiOLD  1351  rb-bijust  1586  nfbii  1649  sbnf2  2185  sb8mo  2321  cbvmo  2323  raleqbii  2899  rmo5  3073  cbvrmo  3080  ss2ab  3554  sbcssg  3928  trint  4547  ssextss  4691  relop  5142  dmcosseq  5253  cotrg  5366  issref  5368  cnvsym  5369  intasym  5370  intirr  5373  codir  5375  qfto  5376  cnvpo  5528  dff14a  6152  porpss  6557  funcnvuni  6726  poxp  6885  cp  8300  aceq2  8491  kmlem12  8532  kmlem15  8535  zfcndpow  8983  grothprim  9201  dfinfmr  10515  infmsup  10516  infmrgelb  10518  infmrlb  10519  xrinfmss2  11505  algcvgblem  14293  isprm2  14312  oduglb  15971  odulub  15973  isirred2  17548  isdomn2  18146  ntreq0  19748  ist0-3  20016  ist1-3  20020  ordthaus  20055  dfcon2  20089  iscusp2  20974  mdsymlem8  27530  mo5f  27584  iuninc  27641  suppss2f  27701  tosglblem  27894  esumpfinvalf  28308  esum2dlem  28324  axrepprim  29318  axacprim  29323  dffr5  29426  dfso2  29427  dfpo2  29428  elpotr  29456  itg2addnclem2  30310  gtinf  30380  isdmn3  30714  sbcimi  30755  moxfr  30867  isdomn3  31408  conss34  31595  onfrALTlem5  33727  onfrALTlem5VD  34105  bnj110  34336  bnj92  34340  bnj539  34369  bnj540  34370  ifpim123g  38122  snhesn  38283  psshepw  38285  frege77  38441  frege93  38457
  Copyright terms: Public domain W3C validator