MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anbi1d Unicode version

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

Proof of Theorem anbi1d
StepHypRef Expression
1 bid.1 . . 3
21a1d 25 . 2
32pm5.32rd 640 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  anbi1  706  anbi12d  710  bi2anan9  873  pm5.71  936  cador  1458  drsb1  2118  eleq1d  2526  eleq1OLD  2531  rexeqf  3051  reueq1f  3052  rmoeq1f  3053  rabeqf  3102  vtocl2gaf  3174  vtocl4ga  3179  alexeqg  3228  alexeq  3229  elrabi  3254  reu2eqd  3296  sbc2or  3336  sbc5  3352  rexss  3566  psstr  3607  ineq1  3692  difin2  3759  r19.28z  3921  r19.28zv  3924  rabsnifsb  4098  ssunsn2  4189  preq12bg  4209  prel12g  4210  opeq1  4217  eluni  4252  csbuni  4277  disjxun  4450  mpteq12f  4528  axrep1  4564  axrep2  4565  axrep3  4566  zfrepclf  4569  axsep  4572  axsep2  4574  zfauscl  4575  reusv2lem4  4656  rabxfrd  4673  opthg  4727  otthg  4735  copsexg  4737  copsexgOLD  4738  euotd  4753  elopab  4760  pocl  4812  dflim2  4939  xpeq1  5018  elxpi  5020  vtoclr  5049  opbrop  5084  opelresg  5286  resopab2  5327  fun11  5658  feq2  5719  f1eq2  5782  f1eq3  5783  foeq2  5797  brprcneu  5864  ssimaexg  5939  dmfco  5947  fndmdif  5991  rexsuppOLD  6012  respreima  6016  isoeq5  6219  isoini  6234  isopolem  6241  f1oiso  6247  f1oiso2  6248  riotaeqdv  6258  oprabid  6323  oprabv  6345  mpt2eq123  6356  mpt2eq123dva  6358  eloprabga  6389  resoprab  6398  resoprab2  6399  elrnmpt2res  6416  ov  6422  ov3  6439  ov6g  6440  ovg  6441  caoftrn  6575  uniuni  6609  limuni3  6687  elxp4  6744  elxp5  6745  opabex3d  6778  opabex3  6779  opiota  6859  eloprabi  6862  cnvf1o  6899  frxp  6910  xporderlem  6911  poxp  6912  fnwelem  6915  suppimacnv  6929  rexsupp  6937  mpt2curryd  7017  smoel2  7053  omeu  7253  oeeui  7270  omabs  7315  omopth  7326  qliftel  7413  brecop  7423  eroveu  7425  erov  7427  ecopovtrn  7433  ixpsnf1o  7529  dom2lem  7575  xpsnen  7621  xpassen  7631  pw2f1olem  7641  xpf1o  7699  unxpdom  7747  domunfican  7813  preleq  8055  zfinf  8077  cantnfs  8106  cantnfsOLD  8136  tcvalg  8190  r0weon  8411  fseqenlem1  8426  acni2  8448  aceq1  8519  aceq0  8520  dfac2a  8531  dfac12lem2  8545  cardcf  8653  cfeq0  8657  cfsuc  8658  cff1  8659  cfss  8666  isf32lem5  8758  fin1a2lem6  8806  zfac  8861  brdom7disj  8930  brdom6disj  8931  axrepnd  8990  axunndlem1  8991  axinfnd  9005  axacndlem5  9010  axacnd  9011  zfcndrep  9013  zfcndinf  9017  zfcndac  9018  pwfseqlem4a  9060  pwfseqlem4  9061  gruina  9217  grothomex  9228  ordpipq  9341  elnpi  9387  genpass  9408  ltprord  9429  reclem2pr  9447  reclem3pr  9448  recexpr  9450  addsrmo  9471  mulsrmo  9472  addsrpr  9473  mulsrpr  9474  ltsosr  9492  mulgt0sr  9503  supsr  9510  ltresr  9538  axpre-lttrn  9564  axpre-mulgt0  9566  prime  10968  peano5uzti  10977  uzindOLD  10982  rexuz  11160  ltxr  11353  qbtwnre  11427  xmulneg1  11490  supxr2  11534  ixxval  11566  fzval  11703  nn0opth2  12352  hashbclem  12501  hashf1lem2  12505  eqwrd  12582  swrdeq  12671  wrd2ind  12703  cshwcsh2id  12796  abslt  13147  absle  13148  lenegsq  13153  abs2difabs  13167  ello12  13339  elo12  13350  o1lo1  13360  rlimuni  13373  lo1resb  13387  o1resb  13389  2clim  13395  rlimcn2  13413  climcn2  13415  addcn2  13416  mulcn2  13418  o1of2  13435  sumeq1  13511  fsum2dlem  13585  modfsummod  13608  prodeq1f  13715  fprod2dlem  13784  znnenlem  13945  nndivdvds  13992  divalg2  14063  smupval  14138  gcdval  14146  gcdass  14183  rpexp  14261  pythagtriplem2  14341  pythagtrip  14358  vdwapun  14492  0ram  14538  ramub1lem2  14545  pwsle  14889  imasleval  14938  ismre  14987  ismri  15028  iscatd2  15078  isssc  15189  funcpropd  15269  fullpropd  15289  fthres2b  15299  fthres2c  15300  setcsect  15416  prslem  15560  drsdir  15564  posi  15579  tosso  15666  ipoval  15784  ipolt  15789  odudlatb  15826  dirge  15867  gsumpropd2lem  15900  issgrpv  15913  issgrpn0  15914  mhmpropd  15972  mrcmndind  15997  mgmnsgrpex  16049  issubg3  16219  isga  16329  symgfixelq  16458  psgnfval  16525  psgnval  16532  isslw  16628  dprdw  17043  dprdwOLD  17050  subgdmdprd  17081  drngpropd  17423  issubrg  17429  islmod  17516  lmodlema  17517  lmodprop2d  17572  lsslss  17607  lbspropd  17745  lbsacsbs  17802  aspval2  17996  psrbag  18013  pf1ind  18391  znleval  18593  islbs4  18867  islinds3  18869  mdetunilem4  19117  mdetunilem9  19122  istopg  19404  basis2  19452  tg2  19466  iscld  19528  neival  19603  isnei  19604  isneip  19606  neiptoptop  19632  neiptopnei  19633  neitr  19681  restlp  19684  iscn  19736  cnpval  19737  iscnp  19738  regsep  19835  nrmsep3  19856  1stcclb  19945  2ndc1stc  19952  2ndcctbss  19956  2ndcdisj  19957  llyi  19975  nllyi  19976  hausmapdom  20001  locfinnei  20024  comppfsc  20033  elkgen  20037  txbas  20068  txcls  20105  txcnpi  20109  ptpjopn  20113  txdis1cn  20136  txtube  20141  txcmplem1  20142  hausdiag  20146  tx1stc  20151  txkgen  20153  xkococnlem  20160  xkococn  20161  elqtop  20198  kqreglem1  20242  elmptrab  20328  isfbas  20330  elflim2  20465  elflim  20472  hauspwpwf1  20488  alexsublem  20544  ghmcnp  20613  qustgplem  20619  tsmssubm  20644  elutop  20736  ustuqtop4  20747  isucn  20781  iscfilu  20791  ispsmet  20808  ismet  20826  isxmet  20827  ismet2  20836  imasdsf1olem  20876  blres  20934  elmopn  20945  mopni  20995  neibl  21004  nrmmetd  21095  ngppropd  21151  elcncf  21393  mulc1cncf  21409  elpi1  21545  metcld2  21745  pmltpclem1  21860  ovolval  21885  itg1climres  22121  itg2val  22135  isibl  22172  itgeq1f  22178  itgresr  22185  iblcn  22205  itgfsum  22233  dvreslem  22313  dvfsumlem2  22428  deg1ldg  22492  vieta1  22708  ulm2  22780  sincosq2sgn  22892  sincosq4sgn  22894  efopn  23039  dvdsflsumcom  23464  fsumvma2  23489  logfac2  23492  dchrptlem1  23539  lgsdchrval  23622  pntibndlem3  23777  pntlemi  23789  pntleme  23793  pnt3  23797  istrkg2d  23856  istrkgld  23857  istrkg2ld  23858  axtgsegcon  23861  axtg5seg  23862  axtgpasch  23864  axtgupdim2  23869  legov  23972  islnopp  24113  ishpg  24128  brcgr  24203  brbtwn2  24208  axsegconlem1  24220  axsegcon  24230  axcontlem10  24276  usgra2edg  24382  trls  24538  istrl2  24540  trlon  24542  is2wlk  24567  spths  24569  0spth  24573  pthon  24577  spthon  24584  isspthonpth  24586  usgra2wlkspthlem1  24619  0crct  24626  0cycl  24627  usgrcyclnl2  24641  wwlknprop  24686  vfwlkniswwlkn  24706  wwlknext  24724  wwlknfi  24738  clwlk  24753  isclwlk  24756  clwlkcompim  24764  clwwlkn2  24775  clwwlknimp  24776  clwwlkel  24793  clwwlkf  24794  clwwlkext2edg  24802  wwlkext2clwwlk  24803  wwlksubclwwlk  24804  erclwwlknsym  24826  erclwwlkntr  24827  clwlkfoclwwlk  24845  el2wlkonotot0  24872  2spontn0vne  24887  rusgranumwlkl1  24947  rusgranumwlklem3  24951  rusgranumwlkb0  24953  rusgra0edg  24955  eupath2lem2  24978  3cyclfrgrarn1  25012  4cycl2vnunb  25017  frg2wot1  25057  usg2spot2nb  25065  extwwlkfablem2  25078  numclwwlkovfel2  25083  numclwwlkovf2  25084  numclwwlkovf2ex  25086  numclwwlkovgel  25088  numclwwlkovgelim  25089  numclwlk2lem2f  25103  numclwlk2lem2f1o  25105  numclwwlk5  25112  drngoi  25409  rngosn3  25428  vci  25441  isvclem  25470  nmoofval  25677  isph  25737  norm3lemt  26069  isch2  26141  cmbr  26502  eigre  26754  eigorth  26757  nmopub  26827  nmfnleub  26844  cvbr  27201  mdbr  27213  dmdbr  27218  chrelat2  27289  mdsymlem2  27323  rexunirn  27390  ifeqeqx  27419  funcnvmptOLD  27509  funcnvmpt  27510  1stpreima  27524  fpwrelmapffslem  27555  isomnd  27691  archirng  27732  isslmd  27745  slmdlema  27746  orngmul  27793  dya2iocuni  28254  omsfval  28265  itgeq12dv  28268  isrrvv  28382  brafs  28552  kur14  28660  pconcn  28669  cnpcon  28675  txpcon  28677  cvmscbv  28703  cvmcov  28708  cvmsi  28710  cvmsval  28711  cvmopnlem  28723  cvmlift2lem10  28757  cvmlift3lem2  28765  cvmlift3lem6  28769  cvmlift3lem7  28770  cvmlift3lem9  28772  cvmlift3  28773  mclsssvlem  28922  mclsind  28930  relexp0  29052  relexpsucr  29053  relexpsucl  29055  relexpcnv  29056  relexpdm  29058  relexprn  29059  relexpadd  29061  relexpindlem  29062  rtrclreclem.trans  29069  rtrclreclem.min  29070  eldm3  29191  opelco3  29208  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  dfon2  29224  preduz  29280  poseq  29333  soseq  29334  sltval  29407  nodenselem5  29445  nocvxminlem  29450  elfuns  29565  brofs  29655  5segofs  29656  brifs  29693  ifscgr  29694  brcolinear  29709  lineext  29726  brfs  29729  fscgr  29730  linecgr  29731  btwnconn1lem4  29740  btwnconn1lem8  29744  btwnconn1lem11  29747  btwnconn1lem12  29748  segcon2  29755  brsegle  29758  outsideofeq  29780  funray  29790  funline  29792  fvline  29794  linethru  29803  wl-ax11-lem8  30032  ptrest  30048  heicant  30049  mblfinlem3  30053  mblfinlem4  30054  mbfresfi  30061  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  areacirclem5  30111  trer  30134  finminlem  30136  ivthALT  30153  filnetlem4  30199  cover2  30204  cover2g  30205  fdc  30238  fdc1  30239  heibor1  30306  bfp  30320  isdrngo1  30359  isriscg  30387  isfldidl2  30466  mrefg2  30639  mzpclval  30657  eldiophb  30690  eldioph2lem1  30693  eldioph3  30699  lzenom  30703  diophin  30706  eldiophss  30708  diophrex  30709  eq0rabdioph  30710  pellexlem3  30767  elpell1qr  30783  elpell14qr  30785  elpell1234qr  30787  jm2.27  30950  rmydioph  30956  expdiophlem1  30963  expdioph  30965  pw2f1ocnv  30979  hbtlem1  31072  hbtlem7  31074  dgraalem  31094  dgraaub  31097  lcmval  31198  lcmass  31218  binomcxplemnotnn0  31261  2sbc6g  31322  2sbc5g  31323  iotasbc  31326  dropab1  31356  dropab2  31357  mullimc  31622  mullimcf  31629  fourierdlem42  31931  fourierdlem48  31937  fourierdlem50  31939  fourierdlem51  31940  fourierdlem54  31943  fourierdlem86  31975  dfdfat2  32216  2ffzoeq  32341  spthdifv  32352  usgra2pth  32354  edgssv2ALT  32401  edgssv2  32402  isfusgra0  32425  fusgraimpclALT2  32431  mgmhmpropd  32473  ismhm0  32493  dfiso2  32568  isrnghm  32698  rngcsect  32788  rngcinv  32789  rngcsectOLD  32800  rngcinvOLD  32801  ringcsect  32839  ringcinv  32840  ringcsectOLD  32863  ringcinvOLD  32864  lmod1  33093  bnj956  33835  bnj1146  33850  bnj18eq1  33985  bj-axrep1  34374  bj-axrep2  34375  bj-axrep3  34376  bj-axsep  34379  bj-eleq1w  34422  bj-rabeqd  34488  bj-axsep2  34493  islshpat  34742  lcvbr  34746  lshpsmreu  34834  ldual1dim  34891  cvrval  34994  cvrnbtwn3  35001  iscvlat2N  35049  ishlat3N  35079  hlrelat5N  35125  3dim0  35181  llnexatN  35245  islpln5  35259  islvol5  35303  pmapjat1  35577  ltrnu  35845  cdleme02N  35947  cdlemg33b  36433  cdlemg33c  36434  dvhb1dimN  36712  dibelval3  36874  dibopelval3  36875  dib1dim  36892  dibglbN  36893  diblsmopel  36898  dicval  36903  dicopelval  36904  dicelval3  36907  dicelval1sta  36914  dihopelvalcpre  36975  dih1dimatlem  37056  dihpN  37063  dihjatcclem4  37148  lpolsetN  37209  mapdpglem3  37402  hdmapglem7a  37657  bj-ifbi2  37700
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator