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  845  rb-bijust  1566  nfbii  1624  sbnf2  2166  sb8mo  2317  cbvmo  2319  raleqbii  2909  rmo5  3080  cbvrmo  3087  ss2ab  3568  sbcssg  3938  trint  4555  ssextss  4701  relop  5153  dmcosseq  5264  cotrg  5378  issref  5380  cnvsym  5381  intasym  5382  intirr  5385  codir  5387  qfto  5388  cnvpo  5545  dff14a  6166  porpss  6569  funcnvuni  6738  poxp  6896  cp  8310  aceq2  8501  kmlem12  8542  kmlem15  8545  zfcndpow  8995  grothprim  9213  dfinfmr  10521  infmsup  10522  infmrgelb  10524  infmrlb  10525  xrinfmss2  11503  algcvgblem  14068  isprm2  14087  oduglb  15629  odulub  15631  isirred2  17163  isdomn2  17759  ntreq0  19384  ist0-3  19652  ist1-3  19656  ordthaus  19691  dfcon2  19726  iscusp2  20632  mdsymlem8  27102  mo5f  27156  iuninc  27198  suppss2f  27247  oduprs  27403  tosglblem  27416  esumpfinvalf  27833  axrepprim  28825  axacprim  28830  dffr5  29035  dfso2  29036  dfpo2  29037  elpotr  29066  itg2addnclem2  29920  gtinf  29990  isdmn3  30301  sbcimi  30342  moxfr  30455  isdomn3  30996  conss34  31156  onfrALTlem5  32611  onfrALTlem5VD  32982  bnj110  33212  bnj92  33216  bnj539  33245  bnj540  33246
  Copyright terms: Public domain W3C validator