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  8683  nnaddcl  8708  nnmulcl  8709  zaddcllempos  9059  zaddcllemneg  9061  prime  9118  peano5uzti  9127  uzind2  9131  zindd  9137  uzaddcl  9349  exfzdc  9985  frec2uzltd  10144  frec2uzrdg  10150  frecuzrdgtcl  10153  frecuzrdgg  10157  frecuzrdgfunlem  10160  seq3val  10199  seqvalcd  10200  seq3clss  10208  seq3fveq2  10210  seq3shft2  10214  monoord  10217  seq3split  10220  seq3caopr3  10222  seq3f1olemp  10243  seq3id3  10248  seq3id2  10250  seq3homo  10251  seq3z  10252  ser3ge0  10258  exp3vallem  10262  expcllem  10272  expap0  10291  mulexp  10300  expadd  10303  expmul  10306  leexp2r  10315  leexp1a  10316  bernneq  10380  facdiv  10452  faclbnd  10455  faclbnd6  10458  omgadd  10516  seq3coll  10553  shftvalg  10576  shftval4g  10577  cjexp  10633  resqrexlemover  10750  resqrexlemdecn  10752  resqrexlemlo  10753  resqrexlemcalc3  10756  absexp  10819  climshft  11041  climub  11081  climserle  11082  fsum2d  11172  fsumabs  11202  fsumiun  11214  binom  11221  bcxmas  11226  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  demoivreALT  11407  dvdsfac  11485  infssuzex  11569  bezoutlemstep  11612  bezoutlemmain  11613  bezoutlemex  11616  dfgcd2  11629  gcdmultiple  11635  rplpwr  11642  nn0seqcvgd  11649  alginv  11655  algcvga  11659  algfx  11660  isprm4  11727  prmind2  11728  prmdvdsexp  11753  prmfac1  11757  ennnfoneleminc  11851  ennnfonelemkh  11852  ennnfonelemhf1o  11853  ennnfonelemhom  11855  fiinopn  12098  cnpfval  12291  iscnp3  12299  cnprcl2k  12302  tgcn  12304  lmbr  12309  lmbr2  12310  lmbrf  12311  lmss  12342  cnmptcom  12394  metss  12590  metcnp  12608  metcnpi  12611  metcnpi2  12612  elcncf  12656  cncfi  12661  rescncf  12664  cncfco  12674  cdivcncfap  12683  ellimc3apf  12725  limcdifap  12727  limcmpted  12728  limcimo  12730  limcresi  12731  cnplimclemr  12734  limccoap  12743  bdbm1.3ii  13016  bj-2inf  13063  bj-omtrans  13081  nninfalllemn  13129  nninfalllem1  13130  nninfsellemdc  13133  nninfsellemqall  13138
  Copyright terms: Public domain W3C validator