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

Theorem anbi1d 438
Description: Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
Hypothesis
Ref Expression
anbid.1
Assertion
Ref Expression
anbi1d

Proof of Theorem anbi1d
StepHypRef Expression
1 anbid.1 . . 3
21a1d 22 . 2
32pm5.32rd 424 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:  anbi1  439  anbi12d  442  bi2anan9  523  pm5.71dc  850  xorbi1d  1251  drsb1  1653  ax11ev  1682  eleq1  2073  rexeqf  2471  reueq1f  2472  rmoeq1f  2473  rabeqf  2519  vtocl2gaf  2588  alexeq  2638  ceqex  2639  elrabi  2663  sbc5  2755  rexss  2975  psstr  3017  sspsstr  3018  ineq1  3099  difin2  3167  r19.28m  3279  preq12bg  3507  opeq1  3512  eluni  3546  mpteq12f  3800  axsep2  3839  zfauscl  3840  opthg  3938  copsexg  3944  euotd  3954  elopab  3958  pocl  4003  uniuni  4121  rabxfrd  4139  regexmidlemm  4189  regexmidlem1  4190  preleq  4205  xpeq1  4274  elxpi  4276  vtoclr  4303  opbrop  4334  opelresg  4534  resopab2  4570  elxp4  4723  elxp5  4724  cnvpom  4775  fun11  4880  feq2  4945  f1eq2  5001  f1eq3  5002  foeq2  5016  brprcneu  5084  ssimaexg  5148  dmfco  5154  fndmdif  5185  rexsupp  5204  respreima  5208  isoeq5  5358  isoini  5370  isopolem  5374  f1oiso  5378  f1oiso2  5379  riotaeqdv  5382  acexmidlemab  5418  acexmidlemcase  5419  oprabid  5449  mpt2eq123  5475  mpt2eq123dva  5477  eloprabga  5502  resoprab  5508  resoprab2  5509  ov  5531  ovi3  5548  ov6g  5549  ovg  5550  caoftrn  5647  opabex3d  5659  opabex3  5660  elxp7  5708  eloprabi  5733  cnvf1o  5757  xporderlem  5762  poxp  5763  smoel2  5828  frec0g  5890  frecsuclem3  5894  frecsuc  5895  nnaordex  5999  qliftel  6085  brecop  6095  eroveu  6096  ecopovtrn  6102  ecopovtrng  6105  th3qlem2  6108  th3q  6110  dfplpq2  6199  dfmpq2  6200  ltsonq  6243  enq0sym  6273  enq0ref  6274  enq0tr  6275  enq0breq  6277  addnq0mo  6288  mulnq0mo  6289  addnnnq0  6290  mulnnnq0  6291  elinp  6314  prnmaxl  6328  prnminu  6329  prarloclemlo  6334  prarloc  6343  genpdflem  6347  genpassl  6365  genpassu  6366  ltexprlemm  6423  recexprlemell  6443  recexprlemelu  6444  addsrmo  6481  mulsrmo  6482  addsrpr  6483  mulsrpr  6484  lttrsr  6500  mulgt0sr  6514  ltresr  6545  axpre-lttrn  6573  axpre-mulgt0  6576  recexgt0  7167  apreap  7174  apreim  7190  prime  7901  bdsep2  8270  bdzfauscl  8274  bj-d0clsepcl  8310
  Copyright terms: Public domain W3C validator