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

Theorem imbi2d 223
Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imbi2d (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))

Proof of Theorem imbi2d
StepHypRef Expression
1 imbid.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 22 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
32pm5.74d 175 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  imbi12d  227  imbi2  230  pm5.42  307  imandc  797  pm4.14dc  798  imimorbdc  806  pm5.6dc  846  ax11v2  1717  ax11v  1724  equs5or  1727  mo23  1957  2gencl  2604  3gencl  2605  vtocl2gf  2632  vtocl3gf  2633  eqeu  2733  mo2icl  2742  euind  2750  reu7  2758  reuind  2766  sbctt  2851  sbcnestgf  2924  preq12bg  3571  elint  3648  elintrabg  3655  intab  3671  trss  3890  bm1.3ii  3905  pocl  4067  swopolem  4069  sowlin  4084  frforeq3  4111  frirrg  4114  frind  4116  reusv3  4219  regexmid  4287  ordsoexmid  4313  tfisi  4337  finds2  4351  nnregexmid  4369  vtoclr  4415  2optocl  4444  3optocl  4445  raliunxp  4504  resieq  4649  iss  4681  cnveqb  4803  funmo  4944  fnbrfvb  5241  fvelimab  5256  fvmptssdm  5282  fmptco  5357  fnressn  5376  fressnfv  5377  isoselem  5486  isosolem  5490  ovg  5666  caovcan  5692  caovordig  5693  caovord  5699  f1o2ndf1  5876  poxp  5880  smoeq  5935  smores  5937  tfrlem1  5953  tfrlemi1  5976  tfrexlem  5978  tfri3  5983  rdgon  6003  freccl  6023  nnacl  6089  nnmcl  6090  nnacom  6093  nnaass  6094  nndi  6095  nnmass  6096  nnmsucr  6097  nnmcom  6098  nnsucsssuc  6101  nntri3or  6102  nnaordi  6111  nnaword  6114  nnmordi  6119  nnaordex  6130  2ecoptocl  6224  3ecoptocl  6225  th3qlem2  6239  xpdom2g  6336  findcard2  6376  findcard2s  6377  supeq1  6391  ordiso2  6414  distrnq0  6614  addassnq0  6617  elinp  6629  prcdnql  6639  prcunqu  6640  prarloclem3  6652  caucvgpr  6837  caucvgprpr  6867  ltsosr  6906  caucvgsrlemcau  6934  caucvgsrlemgt1  6936  caucvgsrlemoffres  6941  pitonn  6981  axpre-ltwlin  7014  axcaucvglemres  7030  nnaddcl  8009  nnmulcl  8010  zaddcllempos  8338  zaddcllemneg  8340  prime  8395  peano5uzti  8404  uzind2  8408  zindd  8414  uzaddcl  8624  frec2uzltd  9352  frec2uzrdg  9358  frecuzrdgfn  9361  iseqss  9389  iseqfveq2  9391  iseqshft2  9395  monoord  9398  iseqsplit  9401  iseqcaopr3  9403  iseqid3s  9409  iseqhomo  9411  iseqz  9412  expivallem  9420  expcllem  9430  expap0  9449  mulexp  9458  expadd  9461  expmul  9464  leexp2r  9473  leexp1a  9474  bernneq  9536  facdiv  9605  faclbnd  9608  faclbnd6  9611  shftvalg  9664  shftval4g  9665  cjexp  9720  resqrexlemover  9836  resqrexlemdecn  9838  resqrexlemlo  9839  resqrexlemcalc3  9842  absexp  9905  climshft  10055  climub  10094  climserile  10095  dvdsfac  10171  nn0seqcvgd  10249  ialginv  10255  ialgcvga  10259  ialgfx  10260  bdbm1.3ii  10384  bj-2inf  10435  bj-omtrans  10454
  Copyright terms: Public domain W3C validator