ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi12d Structured version   Unicode version

Theorem imbi12d 223
Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1
imbi12d.2
Assertion
Ref Expression
imbi12d

Proof of Theorem imbi12d
StepHypRef Expression
1 imbi12d.1 . . 3
21imbi1d 220 . 2
3 imbi12d.2 . . 3
43imbi2d 219 . 2
52, 4bitrd 177 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  nfbidf  1429  drnf1  1618  drnf2  1619  equveli  1639  ax11v2  1698  ax11v  1705  ax11ev  1706  equs5or  1708  mobidh  1931  mobid  1932  axext3  2020  cbvralf  2521  cbvraldva2  2531  gencbval  2596  vtoclgaf  2612  vtocl2gaf  2614  vtocl3gaf  2616  rspct  2643  rspc  2644  ceqex  2665  ralab2  2699  mob2  2715  mob  2717  morex  2719  reu7  2730  reu8  2731  nelrdva  2740  cdeqim  2751  sbcimg  2798  csbhypf  2879  cbvralcsf  2902  dfss2f  2930  sbcssg  3324  sneqrg  3524  elintab  3617  intss1  3621  intmin  3626  dfiin2g  3681  trel  3852  trss  3854  bnd2  3917  zfpow  3919  rext  3942  opth  3965  copsexg  3972  poeq1  4027  pocl  4031  swopolem  4033  swopo  4034  soeq1  4043  sowlin  4048  ordelord  4084  reusv3i  4157  ordtriexmid  4210  onsucsssucexmid  4212  onsucelsucexmid  4215  ordsucunielexmid  4216  regexmidlem1  4218  regexmid  4219  elirr  4224  en2lp  4232  ordsoexmid  4240  tfis  4249  tfisi  4253  peano2  4261  findes  4269  nnregexmid  4285  vtoclr  4331  poinxp  4352  soinxp  4353  posng  4355  ssrel  4371  ssrel2  4373  ssrelrel  4383  relop  4429  issref  4650  iota5  4830  dffun4f  4861  sbcfung  4868  funopg  4877  brprcneu  5114  funfveu  5131  tz6.12f  5145  funbrfv  5155  ssimaexg  5178  fvmptss2  5190  fvmptssdm  5198  fvmptf  5206  fvelrn  5241  f1veqaeq  5351  dff13f  5352  isopolem  5404  isosolem  5406  riota5f  5435  oprabid  5480  ovmpt2s  5566  ov2gf  5567  ovi3  5579  caovcan  5607  caovordig  5608  caofrss  5677  caoftrn  5678  dfoprab4f  5761  f1o2ndf1  5791  poxp  5794  smoel  5856  tfrlem1  5864  nnsucelsuc  6009  nnsucsssuc  6010  nnmordi  6025  nnaordex  6036  qsel  6119  eroveu  6133  ecopovtrn  6139  ecopovtrng  6142  th3qlem2  6145  fundmeng  6223  ssfiexmid  6254  ltsonq  6382  ltexnqq  6391  prcdnql  6466  prcunqu  6467  prloc  6473  prdisj  6474  genprndl  6503  genprndu  6504  lttrsr  6670  ltsosr  6672  recexgt0sr  6681  mulgt0sr  6684  aptisr  6685  mulextsr1  6687  axprecex  6744  axpre-ltwlin  6747  axpre-lttrn  6748  axpre-apti  6749  axpre-mulgt0  6751  axpre-mulext  6752  ltleletr  6877  squeeze0  7631  nnsub  7713  fzind  8109  uzind4s  8289  uzind4s2  8290  indstr  8292  frec2uzzd  8847  frec2uzuzd  8849  frec2uzltd  8850  iseqfveq2  8885  expcl2lemap  8901  cbvrald  9242  bj-bdfindes  9383  bj-omtrans  9390  bj-inf2vnlem1  9400  bj-inf2vnlem2  9401  bj-inf2vnlem3  9402  bj-inf2vnlem4  9403  bj-findes  9411  strcoll2  9413  sscoll2  9418
  Copyright terms: Public domain W3C validator