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

Theorem imbi2d 228
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 180 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imbi12d  232  imbi2  235  pm5.42  313  imandc  820  pm4.14dc  821  imimorbdc  829  pm5.6dc  869  ax11v2  1743  ax11v  1750  equs5or  1753  mo23  1984  2gencl  2643  3gencl  2644  vtocl2gf  2671  vtocl3gf  2672  eqeu  2773  mo2icl  2782  euind  2790  reu7  2798  reuind  2806  sbctt  2891  sbcnestgf  2964  preq12bg  3591  elint  3668  elintrabg  3675  intab  3691  trss  3910  bm1.3ii  3925  pocl  4094  swopolem  4096  sowlin  4111  frforeq3  4138  frirrg  4141  frind  4143  reusv3  4246  regexmid  4314  ordsoexmid  4341  tfisi  4365  finds2  4379  nnregexmid  4397  vtoclr  4444  2optocl  4473  3optocl  4474  raliunxp  4535  resieq  4681  iss  4715  cnveqb  4840  funmo  4984  fnbrfvb  5290  fvelimab  5305  fvmptssdm  5332  fmptco  5406  fnressn  5425  fressnfv  5426  isoselem  5538  isosolem  5542  ovg  5718  caovcan  5744  caovordig  5745  caovord  5751  f1o2ndf1  5928  poxp  5932  smoeq  5987  smores  5989  tfrlem1  6005  tfrlemi1  6029  tfrexlem  6031  tfri3  6064  oawordriexmid  6163  nnacl  6173  nnmcl  6174  nnacom  6177  nnaass  6178  nndi  6179  nnmass  6180  nnmsucr  6181  nnmcom  6182  nnsucsssuc  6185  nntri3or  6186  nnaordi  6197  nnaword  6200  nnmordi  6205  nnaordex  6216  2ecoptocl  6310  3ecoptocl  6311  th3qlem2  6325  xpdom2g  6478  findcard2  6535  findcard2s  6536  xpfi  6565  supeq1  6588  ordiso2  6635  updjud  6680  distrnq0  6921  addassnq0  6924  elinp  6936  prcdnql  6946  prcunqu  6947  prarloclem3  6959  caucvgpr  7144  caucvgprpr  7174  ltsosr  7213  caucvgsrlemcau  7241  caucvgsrlemgt1  7243  caucvgsrlemoffres  7248  pitonn  7288  axpre-ltwlin  7321  axcaucvglemres  7337  nnaddcl  8336  nnmulcl  8337  zaddcllempos  8683  zaddcllemneg  8685  prime  8741  peano5uzti  8750  uzind2  8754  zindd  8760  uzaddcl  8969  exfzdc  9540  frec2uzltd  9699  frec2uzrdg  9705  frecuzrdgtcl  9708  frecuzrdgg  9712  frecuzrdgfunlem  9715  iseqvalt  9751  iseqoveq  9759  iseqss  9760  iseqsst  9761  iseqfveq2  9763  iseqshft2  9767  monoord  9770  iseqsplit  9773  iseqcaopr3  9775  iseqid3s  9781  iseqid2  9783  iseqhomo  9784  iseqz  9785  expivallem  9793  expcllem  9803  expap0  9822  mulexp  9831  expadd  9834  expmul  9837  leexp2r  9846  leexp1a  9847  bernneq  9909  facdiv  9981  faclbnd  9984  faclbnd6  9987  omgadd  10045  shftvalg  10098  shftval4g  10099  cjexp  10154  resqrexlemover  10270  resqrexlemdecn  10272  resqrexlemlo  10273  resqrexlemcalc3  10276  absexp  10339  climshft  10517  climub  10556  climserile  10557  dvdsfac  10641  infssuzex  10725  bezoutlemstep  10766  bezoutlemmain  10767  bezoutlemex  10770  dfgcd2  10783  gcdmultiple  10789  rplpwr  10796  nn0seqcvgd  10803  ialginv  10809  ialgcvga  10813  ialgfx  10814  isprm4  10881  prmind2  10882  prmdvdsexp  10907  prmfac1  10911  bdbm1.3ii  11125  bj-2inf  11176  bj-omtrans  11194  nninfalllemn  11240  nninfalllem1  11241  nninfsellemdc  11244  nninfsellemqall  11249
  Copyright terms: Public domain W3C validator