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

Theorem anbi1d 741
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 673 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  anbi1  743  anbi12d  747  bi2anan9  935  pm5.71  997  cador  1587  drsb1  2405  eleq1w  2713  eleq1d  2715  rexeqf  3165  reueq1f  3166  rmoeq1f  3167  rabeqf  3221  vtocl2gaf  3304  vtocl4ga  3309  alexeqg  3363  elrabi  3391  reu2eqd  3436  sbc2or  3477  sbc5  3493  rexss  3702  psstr  3744  ineq1  3840  difin2  3923  r19.28z  4096  rabsnifsb  4289  ssunsn2  4391  preq12bg  4417  prel12g  4418  opeq1  4433  eluni  4471  csbuni  4498  disjxun  4683  mpteq12f  4764  axrep1  4805  axrep2  4806  axrep3  4807  zfrepclf  4810  axsep  4813  axsep2  4815  zfauscl  4816  reusv2lem4  4902  rabxfrd  4919  opthg  4975  otthg  4983  copsexg  4985  euotd  5004  elopab  5012  pocl  5071  xpeq1  5157  elxpi  5164  vtoclr  5198  opbrop  5232  opelresgOLD  5440  resopab2  5483  dflim2  5819  fun11  6001  feq2  6065  f1eq2  6135  f1eq3  6136  foeq2  6150  brprcneu  6222  ssimaexg  6303  dmfco  6311  fndmdif  6361  respreima  6384  isoeq5  6611  isoini  6628  isopolem  6635  f1oiso  6641  f1oiso2  6642  riotaeqdv  6652  oprabid  6717  oprabv  6745  mpt2eq123  6756  mpt2eq123dva  6758  eloprabga  6789  resoprab  6798  resoprab2  6799  elrnmpt2res  6816  ov  6822  ov3  6839  ov6g  6840  ovg  6841  caoftrn  6974  uniuni  7013  limuni3  7094  elxp4  7152  elxp5  7153  opabex3d  7187  opabex3  7188  opiota  7273  eloprabi  7277  mptmpt2opabbrd  7293  cnvf1o  7321  frxp  7332  xporderlem  7333  poxp  7334  fnwelem  7337  suppimacnv  7351  rexsupp  7358  mpt2curryd  7440  smoel2  7505  omeu  7710  oeeui  7727  omabs  7772  omopth  7783  qliftel  7873  brecop  7883  eroveu  7885  erov  7887  ecopovtrn  7893  ixpsnf1o  7990  dom2lem  8037  xpsnen  8085  xpassen  8095  pw2f1olem  8105  xpf1o  8163  unxpdom  8208  domunfican  8274  preleq  8552  zfinf  8574  cantnfs  8601  tcvalg  8652  r0weon  8873  fseqenlem1  8885  acni2  8907  aceq1  8978  aceq0  8979  dfac2a  8990  dfac12lem2  9004  cardcf  9112  cfeq0  9116  cfsuc  9117  cff1  9118  cfss  9125  isf32lem5  9217  fin1a2lem6  9265  zfac  9320  brdom7disj  9391  brdom6disj  9392  axrepnd  9454  axunndlem1  9455  axinfnd  9466  axacndlem5  9471  axacnd  9472  zfcndrep  9474  zfcndinf  9478  zfcndac  9479  pwfseqlem4a  9521  pwfseqlem4  9522  gruina  9678  grothomex  9689  ordpipq  9802  elnpi  9848  genpass  9869  ltprord  9890  reclem2pr  9908  reclem3pr  9909  recexpr  9911  addsrmo  9932  mulsrmo  9933  addsrpr  9934  mulsrpr  9935  ltsosr  9953  mulgt0sr  9964  supsr  9971  ltresr  9999  axpre-lttrn  10025  axpre-mulgt0  10027  prime  11496  peano5uzti  11505  rexuz  11776  ltxr  11987  qbtwnre  12068  xmulneg1  12137  supxr2  12182  ixxval  12221  fzval  12366  preduz  12500  nn0opth2  13099  hashbclem  13274  hashf1lem2  13278  eqwrd  13379  swrdeq  13490  wrd2ind  13523  cshwcsh2id  13620  eqwrds3  13750  cleq1lem  13767  rtrclreclem3  13844  rtrclreclem4  13845  relexpindlem  13847  abslt  14098  absle  14099  lenegsq  14104  abs2difabs  14118  ello12  14291  elo12  14302  o1lo1  14312  rlimuni  14325  lo1resb  14339  o1resb  14341  2clim  14347  rlimcn2  14365  climcn2  14367  addcn2  14368  mulcn2  14370  o1of2  14387  sumeq1  14463  fsum2dlem  14545  modfsummod  14570  prodeq1f  14682  fprod2dlem  14754  znnenlem  14984  nndivdvds  15036  divalg2  15175  smupval  15257  gcdval  15265  gcdass  15311  lcmval  15352  lcmass  15374  rpexp  15479  pythagtriplem2  15569  pythagtrip  15586  vdwapun  15725  0ram  15771  ramub1lem2  15778  pwsle  16199  imasleval  16248  ismre  16297  ismri  16338  iscatd2  16389  dfiso2  16479  isssc  16527  funcpropd  16607  fullpropd  16627  fthres2b  16637  fthres2c  16638  setcsect  16786  prslem  16978  drsdir  16982  posi  16997  tosso  17083  ipoval  17201  ipolt  17206  odudlatb  17243  dirge  17284  gsumpropd2lem  17320  issgrpv  17333  issgrpn0  17334  mhmpropd  17388  mrcmndind  17413  mgmnsgrpex  17465  issubg3  17659  isga  17770  symgfixelq  17899  psgnfval  17966  psgnval  17973  isslw  18069  dprdw  18455  subgdmdprd  18479  drngpropd  18822  issubrg  18828  islmod  18915  lmodlema  18916  lmodprop2d  18973  lsslss  19009  lbspropd  19147  lbsacsbs  19204  aspval2  19395  psrbag  19412  pf1ind  19767  znleval  19951  islbs4  20219  islinds3  20221  mdetunilem4  20469  mdetunilem9  20474  istopg  20748  basis2  20803  tg2  20817  iscld  20879  neival  20954  isnei  20955  isneip  20957  neiptoptop  20983  neiptopnei  20984  neitr  21032  restlp  21035  iscn  21087  cnpval  21088  iscnp  21089  regsep  21186  1stcclb  21295  2ndc1stc  21302  2ndcctbss  21306  2ndcdisj  21307  llyi  21325  nllyi  21326  hausmapdom  21351  locfinnei  21374  comppfsc  21383  elkgen  21387  txbas  21418  txcls  21455  txcnpi  21459  ptpjopn  21463  txdis1cn  21486  txtube  21491  txcmplem1  21492  hausdiag  21496  tx1stc  21501  txkgen  21503  xkococnlem  21510  xkococn  21511  elqtop  21548  kqreglem1  21592  elmptrab  21678  isfbas  21680  elflim2  21815  elflim  21822  hauspwpwf1  21838  alexsublem  21895  ghmcnp  21965  qustgplem  21971  tsmssubm  21993  elutop  22084  ustuqtop4  22095  isucn  22129  iscfilu  22139  ispsmet  22156  ismet  22175  isxmet  22176  ismet2  22185  imasdsf1olem  22225  blres  22283  elmopn  22294  mopni  22344  neibl  22353  nrmmetd  22426  ngppropd  22488  elcncf  22739  mulc1cncf  22755  elpi1  22891  isclmp  22943  metcld2  23151  pmltpclem1  23263  ovolval  23288  itg1climres  23526  itg2val  23540  isibl  23577  itgeq1f  23583  itgresr  23590  iblcn  23610  itgfsum  23638  dvreslem  23718  dvfsumlem2  23835  deg1ldg  23897  vieta1  24112  ulm2  24184  sincosq2sgn  24296  sincosq4sgn  24298  efopn  24449  dvdsflsumcom  24959  fsumvma2  24984  logfac2  24987  dchrptlem1  25034  lgsdchrval  25124  2lgslem1a  25161  pntibndlem3  25326  pntlemi  25338  pntleme  25342  pnt3  25346  istrkgld  25403  istrkg2ld  25404  istrkg3ld  25405  axtgsegcon  25408  axtg5seg  25409  axtgpasch  25411  axtgupdim2  25415  legov  25525  islnopp  25676  ishpg  25696  iscgra1  25747  brcgr  25825  brbtwn2  25830  axsegconlem1  25842  axsegcon  25852  axcontlem10  25898  edgssv2  26135  uhgr2edg  26145  isfusgrf1  26257  edgnbusgreu  26313  cplgr3v  26387  vtxdun  26433  upgr2wlk  26620  upgrtrls  26654  upgristrl  26655  upgrf1istrl  26656  2pthnloop  26683  usgr2pth  26716  isclwlke  26729  isclwlkupgr  26730  iswwlksnx  26788  wlknewwlksn  26841  wwlksnfi  26869  wspthsnwspthsnonOLD  26881  2pthon3v  26908  elwwlks2on  26925  wpthswwlks2on  26927  wpthswwlks2onOLD  26928  rusgrnumwwlkl1  26935  rusgrnumwwlkb0  26938  clwwlknp  26999  clwwlkel  27009  clwwlkf  27010  erclwwlknsym  27034  erclwwlkntr  27035  clwlksfoclwwlk  27050  clwwlknonelOLD  27071  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  0trl  27100  0spth  27104  0crct  27111  0cycl  27112  upgr4cycl4dv4e  27163  upgriseupth  27185  eupth2lem2  27197  3cyclfrgrrn1  27265  4cycl2vnunb  27270  frgrncvvdeqlem2  27280  frgr2wwlk1  27309  fusgr2wsp2nb  27314  vciOLD  27544  isvclem  27560  nmoofval  27745  isph  27805  norm3lemt  28137  isch2  28208  cmbr  28571  eigre  28822  eigorth  28825  nmopub  28895  nmfnleub  28912  cvbr  29269  mdbr  29281  dmdbr  29286  chrelat2  29357  mdsymlem2  29391  rexunirn  29458  ifeqeqx  29487  funcnvmptOLD  29595  funcnvmpt  29596  1stpreima  29612  fpwrelmapffslem  29635  isomnd  29829  archirng  29870  isslmd  29883  slmdlema  29884  orngmul  29931  dya2iocuni  30473  omsfval  30484  elcarsg  30495  itgeq12dv  30516  isrrvv  30633  reprinrn  30824  reprdifc  30833  istrkg2d  30872  axtgupdim2OLD  30874  brafs  30878  bnj956  30973  bnj1146  30988  bnj18eq1  31123  kur14  31324  pconncn  31332  cnpconn  31338  txpconn  31340  cvmscbv  31366  cvmcov  31371  cvmsi  31373  cvmsval  31374  cvmopnlem  31386  cvmlift2lem10  31420  cvmlift3lem2  31428  cvmlift3lem6  31432  cvmlift3lem7  31433  cvmlift3lem9  31435  cvmlift3  31436  mclsssvlem  31585  mclsind  31593  eldm3  31777  opelco3  31802  fv1stcnv  31804  fv2ndcnv  31805  dfon2lem6  31817  dfon2lem7  31818  dfon2lem8  31819  dfon2  31821  poseq  31878  soseq  31879  sltval  31925  nolt02o  31970  slelttr  32007  nocvxminlem  32018  elfuns  32147  brsuccf  32173  brofs  32237  5segofs  32238  brifs  32275  ifscgr  32276  brcolinear  32291  lineext  32308  brfs  32311  fscgr  32312  linecgr  32313  btwnconn1lem4  32322  btwnconn1lem8  32326  btwnconn1lem11  32329  btwnconn1lem12  32330  segcon2  32337  brsegle  32340  outsideofeq  32362  funray  32372  funline  32374  fvline  32376  linethru  32385  trer  32435  finminlem  32437  ivthALT  32455  filnetlem4  32501  knoppndvlem21  32648  bj-axrep1  32913  bj-axrep2  32914  bj-axrep3  32915  bj-axsep  32918  bj-ax8  33012  bj-rabeqd  33041  bj-axsep2  33046  csboprabg  33306  topdifinffinlem  33325  icoreval  33331  isbasisrelowllem1  33333  isbasisrelowllem2  33334  relowlssretop  33341  wl-ax11-lem8  33499  curf  33517  ptrest  33538  poimirlem1  33540  poimirlem13  33552  poimirlem14  33553  poimirlem22  33561  poimirlem24  33563  poimirlem26  33565  poimirlem27  33566  heicant  33574  mblfinlem3  33578  mblfinlem4  33579  mbfresfi  33586  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  areacirclem5  33634  cover2  33638  cover2g  33639  fdc  33671  fdc1  33672  heibor1  33739  bfp  33753  rngosn3  33853  drngoi  33880  isdrngo1  33885  isriscg  33913  isfldidl2  33998  islshpat  34622  lcvbr  34626  lshpsmreu  34714  ldual1dim  34771  cvrval  34874  cvrnbtwn3  34881  iscvlat2N  34929  ishlat3N  34959  hlrelat5N  35005  3dim0  35061  llnexatN  35125  islpln5  35139  islvol5  35183  pmapjat1  35457  ltrnu  35725  cdleme02N  35827  cdlemg33b  36312  cdlemg33c  36313  dvhb1dimN  36591  dibelval3  36753  dibopelval3  36754  dib1dim  36771  dibglbN  36772  diblsmopel  36777  dicval  36782  dicopelval  36783  dicelval3  36786  dicelval1sta  36793  dihopelvalcpre  36854  dih1dimatlem  36935  dihpN  36942  dihjatcclem4  37027  lpolsetN  37088  mapdpglem3  37281  hdmapglem7a  37536  mrefg2  37587  mzpclval  37605  eldiophb  37637  eldioph2lem1  37640  eldioph3  37646  lzenom  37650  diophin  37653  eldiophss  37655  diophrex  37656  eq0rabdioph  37657  pellexlem3  37712  elpell1qr  37728  elpell14qr  37730  elpell1234qr  37732  jm2.27  37892  rmydioph  37898  expdiophlem1  37905  expdioph  37907  pw2f1ocnv  37921  hbtlem1  38010  hbtlem7  38012  dgraalem  38032  dgraaub  38035  ifpbi2  38128  inintabd  38202  cnvcnvintabd  38223  cnvintabd  38226  clcnvlem  38247  iunrelexpmin1  38317  uneqsn  38638  k0004lem2  38763  binomcxplemnotnn0  38872  2sbc6g  38933  2sbc5g  38934  iotasbc  38937  dropab1  38968  dropab2  38969  cbvmpt21  39592  disjinfi  39694  mapsnend  39705  dmrelrnrel  39733  mullimc  40166  mullimcf  40173  limsuppnfd  40252  limsuppnf  40261  limsupre2  40275  limsupre2mpt  40280  limsupre3  40283  limsupre3mpt  40284  limsupre3uzlem  40285  fourierdlem42  40684  fourierdlem48  40689  fourierdlem50  40691  fourierdlem51  40692  fourierdlem54  40695  fourierdlem86  40727  ovnval2  41080  ovnsubaddlem1  41105  hoiqssbl  41160  vonicclem2  41219  dfdfat2  41532  2ffzoeq  41663  pfxeq  41729  mgmhmpropd  42110  ismhm0  42130  isrnghm  42217  rngcsect  42305  rngcinv  42306  rngcsectALTV  42317  rngcinvALTV  42318  ringcsect  42356  ringcinv  42357  ringcsectALTV  42380  ringcinvALTV  42381  lmod1  42606  elbigo2  42671
  Copyright terms: Public domain W3C validator