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  1410  drnf1  1599  drnf2  1600  equveli  1620  ax11v2  1679  ax11v  1686  ax11ev  1687  equs5or  1689  mobidh  1912  mobid  1913  axext3  2001  cbvralf  2501  cbvraldva2  2511  gencbval  2575  vtoclgaf  2591  vtocl2gaf  2593  vtocl3gaf  2595  rspct  2622  rspc  2623  ceqex  2644  ralab2  2678  mob2  2694  mob  2696  morex  2698  reu7  2709  reu8  2710  nelrdva  2719  cdeqim  2730  sbcimg  2777  csbhypf  2858  cbvralcsf  2881  dfss2f  2909  sbcssg  3305  sneqrg  3503  elintab  3596  intss1  3600  intmin  3605  dfiin2g  3660  trel  3831  trss  3833  bnd2  3896  zfpow  3898  rext  3921  opth  3944  copsexg  3951  poeq1  4006  pocl  4010  swopolem  4012  swopo  4013  soeq1  4022  sowlin  4027  ordelord  4063  reusv3i  4137  ordtriexmid  4190  onsucsssucexmid  4192  onsucelsucexmid  4195  ordsucunielexmid  4196  regexmidlem1  4198  regexmid  4199  elirr  4204  en2lp  4212  ordsoexmid  4220  tfis  4229  tfisi  4233  peano2  4241  findes  4249  nnregexmid  4265  vtoclr  4311  poinxp  4332  soinxp  4333  posng  4335  ssrel  4351  ssrel2  4353  ssrelrel  4363  relop  4409  issref  4630  iota5  4810  dffun4f  4840  sbcfung  4847  funopg  4856  brprcneu  5092  funfveu  5109  tz6.12f  5123  funbrfv  5133  ssimaexg  5156  fvmptss2  5168  fvmptssdm  5176  fvmptf  5184  fvelrn  5219  f1veqaeq  5329  dff13f  5330  isopolem  5382  isosolem  5384  riota5f  5412  oprabid  5457  ovmpt2s  5543  ov2gf  5544  ovi3  5556  caovcan  5584  caovordig  5585  caofrss  5654  caoftrn  5655  dfoprab4f  5738  f1o2ndf1  5768  poxp  5771  smoel  5833  tfrlem1  5841  nnsucelsuc  5981  nnsucsssuc  5982  nnmordi  5996  nnaordex  6007  qsel  6090  eroveu  6104  ecopovtrn  6110  ecopovtrng  6113  th3qlem2  6116  ltsonq  6251  ltexnqq  6260  prcdnql  6332  prcunqu  6333  prloc  6339  prdisj  6340  genprndl  6370  genprndu  6371  lttrsr  6506  ltsosr  6508  recexgt0sr  6517  mulgt0sr  6520  aptisr  6521  axprecex  6573  axpre-ltwlin  6576  axpre-lttrn  6577  axpre-apti  6578  axpre-mulgt0  6580  ltleletr  6702  cbvrald  7226  bj-bdfindes  7367  bj-omtrans  7374  bj-inf2vnlem1  7384  bj-inf2vnlem2  7385  bj-inf2vnlem3  7386  bj-inf2vnlem4  7387  bj-findes  7395  strcoll2  7397  sscoll2  7402
  Copyright terms: Public domain W3C validator