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

Theorem imbi12i 327
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 323 . 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 187
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 188
This theorem is referenced by:  orimdi  855  nanbi  1388  nanbiOLD  1389  rb-bijust  1628  nfbii  1691  sbnf2  2234  sb8mo  2300  cbvmo  2302  raleqbii  2870  rmo5  3047  cbvrmo  3054  ss2ab  3529  sbcssg  3908  trint  4530  ssextss  4671  relop  5000  dmcosseq  5111  cotrg  5226  issref  5228  cnvsym  5229  intasym  5230  intirr  5233  codir  5235  qfto  5236  cnvpo  5389  dff14a  6181  porpss  6585  funcnvuni  6756  poxp  6915  infcllem  8005  cp  8363  aceq2  8550  kmlem12  8591  kmlem15  8594  zfcndpow  9041  grothprim  9259  dfinfre  10588  dfinfmrOLD  10589  infrenegsup  10591  infmsupOLD  10592  infmrgelbOLD  10595  infmrlbOLD  10597  xrinfmss2  11596  algcvgblem  14521  isprm2  14617  oduglb  16370  odulub  16372  isirred2  17914  isdomn2  18508  ntreq0  20077  ist0-3  20345  ist1-3  20349  ordthaus  20384  dfcon2  20418  iscusp2  21301  mdsymlem8  28046  mo5f  28103  iuninc  28163  suppss2fOLD  28224  suppss2f  28225  tosglblem  28422  esumpfinvalf  28890  esum2dlem  28906  bnj110  29662  bnj92  29666  bnj539  29695  bnj540  29696  axrepprim  30322  axacprim  30327  dffr5  30385  dfso2  30386  dfpo2  30387  elpotr  30419  gtinf  30965  itg2addnclem2  31905  isdmn3  32218  sbcimi  32258  moxfr  35450  isdomn3  35998  ifpim123g  36061  snhesn  36237  psshepw  36239  frege77  36391  frege93  36407  frege116  36430  frege118  36432  frege131  36445  frege133  36447  conss34  36650  onfrALTlem5  36763  onfrALTlem5VD  37140
  Copyright terms: Public domain W3C validator