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  cbvmo  2153  raleqbii  2544  ss2ab  3183  trint  4068  ssextss  4165  trsuc2OLD  4414  relop  4787  dmcosseq  4899  cotr  5008  issref  5009  cnvsym  5010  intasym  5011  intirr  5014  codir  5016  qfto  5017  cnvpo  5165  funcnvuni  5220  poxp  6126  porpss  6180  cp  7494  aceq2  7679  kmlem12  7720  kmlem15  7723  zfcndpow  8171  grothprim  8389  dfinfmr  9664  infmsup  9665  infmrgelb  9667  infmrlb  9668  xrinfmss2  10560  algcvgblem  12674  isprm2  12693  oduglb  14170  odulub  14172  isirred2  15410  isdomn2  15967  ntreq0  16741  ist0-3  17000  ist1-3  17004  ordthaus  17039  dfcon2  17072  mdsymlem8  22915  ballotlem2  22973  axrepprim  23385  axacprim  23390  dffr5  23446  dfso2  23447  dfpo2  23448  elpotr  23471  wfrlem5  23594  frrlem5  23619  isoriso  24544  mnlmxl2  24601  vecval1b  24783  vecval3b  24784  svli2  24816  isntr  25205  gtinf  25566  isdmn3  26031  moxfr  26084  isdomn3  26855  conss34  26978  onfrALTlem5  27323  onfrALTlem5VD  27674  bnj110  27902  bnj92  27906  bnj539  27935  bnj540  27936  a12study9  28250
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