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

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

Proof of Theorem anbi12d
StepHypRef Expression
1 anbi12d.1 . . 3
21anbi1d 438 . 2
3 anbi12d.2 . . 3
43anbi2d 437 . 2
52, 4bitrd 177 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   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:  pm4.38  537  pm5.17dc  809  orbididc  859  3anbi123d  1206  xorbi2d  1269  xorbi1d  1270  drsb1  1677  mopick  1975  clelab  2159  cbvrexf  2522  cbvreu  2525  cbvrexdva2  2532  cbvrab  2549  gencbvex  2594  rspce  2645  eqvincf  2663  ceqsrexv  2668  elrabf  2690  rexab2  2701  reu2  2723  reu6  2724  rmo4  2728  reu8  2731  reuind  2738  sbcan  2799  sbcang  2800  sbcabel  2833  rmob  2844  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  difjust  2913  injust  2917  eldif  2921  psseq1  3025  psseq2  3026  ssconb  3070  elin  3120  opeq1  3540  opeq2  3541  2ralunsn  3560  elunii  3576  csbunig  3579  eluniab  3583  cbvopab  3819  cbvopab1  3821  cbvopab2  3822  cbvopab1s  3823  cbvopab2v  3825  cbvmpt  3842  trel  3852  nalset  3878  elssabg  3893  mss  3953  exss  3954  opelopab2a  3993  poeq1  4027  pocl  4031  soeq1  4043  ordeq  4075  zfun  4137  snnex  4147  reusv3  4158  regexmid  4219  peano5  4264  limom  4279  nnregexmid  4285  vtoclr  4331  opeliunxp  4338  poinxp  4352  opbrop  4362  csbxpg  4364  opeliunxp2  4419  relop  4429  brcogw  4447  elrnmpt1  4528  elsnres  4590  dfres2  4601  inimasn  4684  xpcanm  4703  xpcan2m  4704  elxp4  4751  elxp5  4752  cnvsom  4804  sbcfung  4868  funopg  4877  fununi  4910  funcnvuni  4911  fneq1  4930  2elresin  4953  feq1  4973  sbcfng  4987  sbcfg  4988  f1eq1  5030  foeq1  5045  f1oeq1  5060  f1oeq2  5061  f1oeq3  5062  ffoss  5101  brprcneu  5114  fv3  5140  tz6.12f  5145  ssimaex  5177  fvopab3g  5188  fvopab3ig  5189  fvopab6  5207  fmptco  5273  elunirn  5348  f1imaeq  5357  f1imapss  5358  foeqcnvco  5373  fliftfun  5379  fliftval  5383  isoeq1  5384  isoeq4  5387  isoini  5400  isopolem  5404  f1oiso2  5409  riotabidv  5413  cbvriota  5421  acexmid  5454  cbvoprab1  5518  cbvoprab2  5519  cbvoprab12  5520  cbvmpt2x  5524  ov  5562  ovig  5564  ovg  5581  caovimo  5636  caoftrn  5678  opabex3d  5690  opabex3  5691  elxp6  5738  unielxp  5742  dfoprab4  5760  dfoprab4f  5761  fmpt2x  5768  xporderlem  5793  poxp  5794  sprmpt2  5798  isprmpt2  5799  dftpos4  5819  tpostpos  5820  smoiso  5858  tfrlem3ag  5865  tfrlem3a  5866  tfr0  5878  tfrlemisucaccv  5880  tfrlemiex  5886  tfrlemi1  5887  tfrlemi14d  5888  tfrexlem  5889  frec0g  5922  frecsuclem3  5929  frecsuc  5930  nnacan  6021  nnmcan  6028  nnaordex  6036  ertr  6057  brecop  6132  eroveu  6133  ecopovtrn  6139  ecopovtrng  6142  th3qlem1  6144  th3qlem2  6145  th3q  6147  xpsnen  6231  endisj  6234  ssfiexmid  6254  ltsopi  6304  recexnq  6374  recmulnqg  6375  ltsonq  6382  lt2addnq  6388  ltbtwnnqq  6398  prarloclemarch2  6402  enq0sym  6414  enq0ref  6415  enq0tr  6416  enq0breq  6418  addnq0mo  6429  mulnq0mo  6430  addnnnq0  6431  mulnnnq0  6432  nqnq0a  6436  nqnq0m  6437  elinp  6456  prcdnql  6466  prcunqu  6467  prltlu  6469  prdisj  6474  prarloclemlo  6476  prarloclem3  6479  prarloclem5  6482  ltdfpr  6488  genprndl  6503  genprndu  6504  genpdisj  6505  appdivnq  6543  ltpopr  6568  ltexprlemdisj  6579  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  ltexpri  6586  recexprlemm  6595  recexprlemdisj  6601  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  recexpr  6609  aptiprleml  6610  archpr  6614  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  cauappcvgprlemlim  6632  cauappcvgpr  6633  addsrmo  6651  mulsrmo  6652  addsrpr  6653  mulsrpr  6654  lttrsr  6670  recexgt0sr  6681  ltresr  6716  pitonn  6724  axprecex  6744  axcnre  6745  axpre-lttrn  6748  axlttrn  6865  letri3  6876  letr  6878  le2add  7214  lt2add  7215  ltleadd  7216  lt2sub  7230  le2sub  7231  apreap  7351  apreim  7367  apti  7386  msq11  7629  cju  7674  peano5nni  7678  1nn  7686  peano2nn  7687  nn2ge  7707  nominpos  7919  elz2  8068  dfuzi  8104  uzind  8105  xrletri3  8471  xrletr  8474  z2ge  8489  elixx1  8516  elioo2  8540  iooshf  8571  iooneg  8606  iccneg  8607  icoshft  8608  elfz1  8629  fzdifsuc  8693  fzrev  8696  1fv  8746  nnesq  9001  cjval  9053  cjth  9054  remim  9068  bj-sseq  9246  bj-nalset  9326  bj-indeq  9364  bj-2inf  9372  peano5set  9374
  Copyright terms: Public domain W3C validator