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

Theorem imbi2d 229
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 181 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  imbi12d  233  imbi2  236  pm5.42  316  imanst  856  pm4.14dc  858  imimorbdc  864  pm5.6dc  894  ax11v2  1774  ax11v  1781  equs5or  1784  mo23  2016  2gencl  2691  3gencl  2692  vtocl2gf  2720  vtocl3gf  2721  eqeu  2825  mo2icl  2834  euind  2842  reu7  2850  reuind  2860  sbctt  2945  sbcnestgf  3019  preq12bg  3668  elint  3745  elintrabg  3752  intab  3768  trss  4003  bm1.3ii  4017  pocl  4193  swopolem  4195  sowlin  4210  frforeq3  4237  frirrg  4240  frind  4242  reusv3  4349  regexmid  4418  ordsoexmid  4445  tfisi  4469  finds2  4483  nnregexmid  4502  vtoclr  4555  2optocl  4584  3optocl  4585  raliunxp  4648  resieq  4797  iss  4833  cnveqb  4962  funmo  5106  fnbrfvb  5428  fvelimab  5443  fvmptssdm  5471  fmptco  5552  fnressn  5572  fressnfv  5573  isoselem  5687  isosolem  5691  ovg  5875  caovcan  5901  caovordig  5902  caovord  5908  f1o2ndf1  6091  poxp  6095  smoeq  6153  smores  6155  tfrlem1  6171  tfrlemi1  6195  tfrexlem  6197  tfri3  6230  oawordriexmid  6332  nnacl  6342  nnmcl  6343  nnacom  6346  nnaass  6347  nndi  6348  nnmass  6349  nnmsucr  6350  nnmcom  6351  nnsucsssuc  6354  nntri3or  6355  nnaordi  6370  nnaword  6373  nnmordi  6378  nnaordex  6389  2ecoptocl  6483  3ecoptocl  6484  th3qlem2  6498  xpdom2g  6692  findcard2  6749  findcard2s  6750  xpfi  6784  supeq1  6839  ordiso2  6886  updjud  6933  distrnq0  7231  addassnq0  7234  elinp  7246  prcdnql  7256  prcunqu  7257  prarloclem3  7269  caucvgpr  7454  caucvgprpr  7484  ltsosr  7536  caucvgsrlemcau  7565  caucvgsrlemgt1  7567  caucvgsrlemoffres  7572  pitonn  7620  axpre-ltwlin  7655  axcaucvglemres  7671  sup3exmid  8672  nnaddcl  8697  nnmulcl  8698  zaddcllempos  9042  zaddcllemneg  9044  prime  9101  peano5uzti  9110  uzind2  9114  zindd  9120  uzaddcl  9330  exfzdc  9957  frec2uzltd  10116  frec2uzrdg  10122  frecuzrdgtcl  10125  frecuzrdgg  10129  frecuzrdgfunlem  10132  seq3val  10171  seqvalcd  10172  seq3clss  10180  seq3fveq2  10182  seq3shft2  10186  monoord  10189  seq3split  10192  seq3caopr3  10194  seq3f1olemp  10215  seq3id3  10220  seq3id2  10222  seq3homo  10223  seq3z  10224  ser3ge0  10230  exp3vallem  10234  expcllem  10244  expap0  10263  mulexp  10272  expadd  10275  expmul  10278  leexp2r  10287  leexp1a  10288  bernneq  10352  facdiv  10424  faclbnd  10427  faclbnd6  10430  omgadd  10488  seq3coll  10525  shftvalg  10548  shftval4g  10549  cjexp  10605  resqrexlemover  10722  resqrexlemdecn  10724  resqrexlemlo  10725  resqrexlemcalc3  10728  absexp  10791  climshft  11013  climub  11053  climserle  11054  fsum2d  11144  fsumabs  11174  fsumiun  11186  binom  11193  bcxmas  11198  cvgratnnlemnexp  11233  cvgratnnlemmn  11234  demoivreALT  11378  dvdsfac  11454  infssuzex  11538  bezoutlemstep  11581  bezoutlemmain  11582  bezoutlemex  11585  dfgcd2  11598  gcdmultiple  11604  rplpwr  11611  nn0seqcvgd  11618  alginv  11624  algcvga  11628  algfx  11629  isprm4  11696  prmind2  11697  prmdvdsexp  11722  prmfac1  11726  ennnfoneleminc  11819  ennnfonelemkh  11820  ennnfonelemhf1o  11821  ennnfonelemhom  11823  fiinopn  12066  cnpfval  12259  iscnp3  12267  cnprcl2k  12270  tgcn  12272  lmbr  12277  lmbr2  12278  lmbrf  12279  lmss  12310  cnmptcom  12362  metss  12558  metcnp  12576  metcnpi  12579  metcnpi2  12580  elcncf  12624  cncfi  12629  rescncf  12632  cncfco  12642  cdivcncfap  12651  ellimc3apf  12672  limcdifap  12674  limcmpted  12675  limcimo  12677  limcresi  12678  cnplimclemr  12681  limccoap  12690  bdbm1.3ii  12891  bj-2inf  12938  bj-omtrans  12956  nninfalllemn  13004  nninfalllem1  13005  nninfsellemdc  13008  nninfsellemqall  13013
  Copyright terms: Public domain W3C validator