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  318  imanst  858  pm4.14dc  860  imimorbdc  866  pm5.6dc  896  ax11v2  1776  ax11v  1783  equs5or  1786  mo23  2018  2gencl  2693  3gencl  2694  vtocl2gf  2722  vtocl3gf  2723  eqeu  2827  mo2icl  2836  euind  2844  reu7  2852  reuind  2862  sbctt  2947  sbcnestgf  3021  preq12bg  3670  elint  3747  elintrabg  3754  intab  3770  trss  4005  bm1.3ii  4019  pocl  4195  swopolem  4197  sowlin  4212  frforeq3  4239  frirrg  4242  frind  4244  reusv3  4351  regexmid  4420  ordsoexmid  4447  tfisi  4471  finds2  4485  nnregexmid  4504  vtoclr  4557  2optocl  4586  3optocl  4587  raliunxp  4650  resieq  4799  iss  4835  cnveqb  4964  funmo  5108  fnbrfvb  5430  fvelimab  5445  fvmptssdm  5473  fmptco  5554  fnressn  5574  fressnfv  5575  isoselem  5689  isosolem  5693  ovg  5877  caovcan  5903  caovordig  5904  caovord  5910  f1o2ndf1  6093  poxp  6097  smoeq  6155  smores  6157  tfrlem1  6173  tfrlemi1  6197  tfrexlem  6199  tfri3  6232  oawordriexmid  6334  nnacl  6344  nnmcl  6345  nnacom  6348  nnaass  6349  nndi  6350  nnmass  6351  nnmsucr  6352  nnmcom  6353  nnsucsssuc  6356  nntri3or  6357  nnaordi  6372  nnaword  6375  nnmordi  6380  nnaordex  6391  2ecoptocl  6485  3ecoptocl  6486  th3qlem2  6500  xpdom2g  6694  findcard2  6751  findcard2s  6752  xpfi  6786  supeq1  6841  ordiso2  6888  updjud  6935  distrnq0  7235  addassnq0  7238  elinp  7250  prcdnql  7260  prcunqu  7261  prarloclem3  7273  caucvgpr  7458  caucvgprpr  7488  ltsosr  7540  caucvgsrlemcau  7569  caucvgsrlemgt1  7571  caucvgsrlemoffres  7576  pitonn  7624  axpre-ltwlin  7659  axcaucvglemres  7675  sup3exmid  8679  nnaddcl  8704  nnmulcl  8705  zaddcllempos  9049  zaddcllemneg  9051  prime  9108  peano5uzti  9117  uzind2  9121  zindd  9127  uzaddcl  9337  exfzdc  9972  frec2uzltd  10131  frec2uzrdg  10137  frecuzrdgtcl  10140  frecuzrdgg  10144  frecuzrdgfunlem  10147  seq3val  10186  seqvalcd  10187  seq3clss  10195  seq3fveq2  10197  seq3shft2  10201  monoord  10204  seq3split  10207  seq3caopr3  10209  seq3f1olemp  10230  seq3id3  10235  seq3id2  10237  seq3homo  10238  seq3z  10239  ser3ge0  10245  exp3vallem  10249  expcllem  10259  expap0  10278  mulexp  10287  expadd  10290  expmul  10293  leexp2r  10302  leexp1a  10303  bernneq  10367  facdiv  10439  faclbnd  10442  faclbnd6  10445  omgadd  10503  seq3coll  10540  shftvalg  10563  shftval4g  10564  cjexp  10620  resqrexlemover  10737  resqrexlemdecn  10739  resqrexlemlo  10740  resqrexlemcalc3  10743  absexp  10806  climshft  11028  climub  11068  climserle  11069  fsum2d  11159  fsumabs  11189  fsumiun  11201  binom  11208  bcxmas  11213  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  demoivreALT  11394  dvdsfac  11470  infssuzex  11554  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlemex  11601  dfgcd2  11614  gcdmultiple  11620  rplpwr  11627  nn0seqcvgd  11634  alginv  11640  algcvga  11644  algfx  11645  isprm4  11712  prmind2  11713  prmdvdsexp  11738  prmfac1  11742  ennnfoneleminc  11835  ennnfonelemkh  11836  ennnfonelemhf1o  11837  ennnfonelemhom  11839  fiinopn  12082  cnpfval  12275  iscnp3  12283  cnprcl2k  12286  tgcn  12288  lmbr  12293  lmbr2  12294  lmbrf  12295  lmss  12326  cnmptcom  12378  metss  12574  metcnp  12592  metcnpi  12595  metcnpi2  12596  elcncf  12640  cncfi  12645  rescncf  12648  cncfco  12658  cdivcncfap  12667  ellimc3apf  12709  limcdifap  12711  limcmpted  12712  limcimo  12714  limcresi  12715  cnplimclemr  12718  limccoap  12727  bdbm1.3ii  12985  bj-2inf  13032  bj-omtrans  13050  nninfalllemn  13098  nninfalllem1  13099  nninfsellemdc  13102  nninfsellemqall  13107
  Copyright terms: Public domain W3C validator