ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi2d Unicode version

Theorem imbi2d 219
Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
imbi2d  |-  ( ph  ->  ( ( th  ->  ps )  <->  ( th  ->  ch ) ) )

Proof of Theorem imbi2d
StepHypRef Expression
1 imbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21a1d 22 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.74d 171 1  |-  ( ph  ->  ( ( th  ->  ps )  <->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  imbi12d  223  imbi2  226  pm5.42  303  imandc  786  pm4.14dc  787  imimorbdc  795  pm5.6dc  835  ax11v2  1701  ax11v  1708  equs5or  1711  mo23  1941  2gencl  2587  3gencl  2588  vtocl2gf  2615  vtocl3gf  2616  eqeu  2711  mo2icl  2720  euind  2728  reu7  2736  reuind  2744  sbctt  2824  sbcnestgf  2897  preq12bg  3544  elint  3621  elintrabg  3628  intab  3644  trss  3863  bm1.3ii  3878  pocl  4040  swopolem  4042  sowlin  4057  frforeq3  4084  frirrg  4087  frind  4089  reusv3  4192  regexmid  4260  ordsoexmid  4286  tfisi  4310  finds2  4324  nnregexmid  4342  vtoclr  4388  2optocl  4417  3optocl  4418  raliunxp  4477  resieq  4622  iss  4654  cnveqb  4776  funmo  4917  fnbrfvb  5214  fvelimab  5229  fvmptssdm  5255  fmptco  5330  fnressn  5349  fressnfv  5350  isoselem  5459  isosolem  5463  ovg  5639  caovcan  5665  caovordig  5666  caovord  5672  f1o2ndf1  5849  poxp  5853  smoeq  5905  smores  5907  tfrlem1  5923  tfrlemi1  5946  tfrexlem  5948  tfri3  5953  rdgon  5973  freccl  5993  nnacl  6059  nnmcl  6060  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  nnsucsssuc  6071  nntri3or  6072  nnaordi  6081  nnaword  6084  nnmordi  6089  nnaordex  6100  2ecoptocl  6194  3ecoptocl  6195  th3qlem2  6209  xpdom2g  6306  findcard2  6346  findcard2s  6347  ordiso2  6355  distrnq0  6555  addassnq0  6558  elinp  6570  prcdnql  6580  prcunqu  6581  prarloclem3  6593  caucvgpr  6778  caucvgprpr  6808  ltsosr  6847  caucvgsrlemcau  6875  caucvgsrlemgt1  6877  caucvgsrlemoffres  6882  pitonn  6922  axpre-ltwlin  6955  axcaucvglemres  6971  nnaddcl  7932  nnmulcl  7933  zaddcllempos  8280  zaddcllemneg  8282  prime  8335  peano5uzti  8344  uzind2  8348  zindd  8354  uzaddcl  8527  frec2uzltd  9163  frec2uzrdg  9169  frecuzrdgfn  9172  iseqss  9200  iseqfveq2  9202  iseqshft2  9206  monoord  9209  iseqsplit  9212  iseqcaopr3  9214  iseqid3s  9220  iseqhomo  9222  expivallem  9230  expcllem  9240  expap0  9259  mulexp  9268  expadd  9271  expmul  9274  leexp2r  9282  leexp1a  9283  bernneq  9343  shftvalg  9411  shftval4g  9412  cjexp  9467  resqrexlemover  9582  resqrexlemdecn  9584  resqrexlemlo  9585  resqrexlemcalc3  9588  absexp  9649  climshft  9799  climub  9838  climserile  9839  nn0seqcvgd  9854  ialginv  9860  ialgcvga  9864  ialgfx  9865  bdbm1.3ii  9985  bj-2inf  10036  bj-omtrans  10055
  Copyright terms: Public domain W3C validator