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

Theorem anbi1d 740
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 672 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  742  anbi12d  746  bi2anan9  950  pm5.71  1012  cador  1693  drsb1  2522  eleq1w  2831  eleq1d  2833  rexeqf  3282  reueq1f  3283  rmoeq1f  3284  rabeqf  3338  vtocl2gaf  3421  vtocl4ga  3426  alexeqg  3479  elrabi  3507  reu2eqd  3552  sbc2or  3593  sbc5  3609  rexss  3815  psstr  3858  ineq1  3955  difin2  4035  r19.28z  4201  rabsnifsb  4390  ssunsn2  4490  preq12bg  4514  prel12gOLD  4515  opeq1  4536  eluni  4574  csbuni  4599  disjxun  4781  mpteq12f  4862  axrep1  4902  axrep2  4903  axrep3  4904  zfrepclf  4907  axsep  4910  axsep2  4912  zfauscl  4913  reusv2lem4  4999  rabxfrd  5016  opthg  5072  otthg  5080  copsexg  5082  opeqsng  5093  euotd  5105  elopab  5115  pocl  5176  xpeq1  5262  elxpi  5269  vtoclr  5303  opbrop  5337  opelresgOLD  5545  resopab2  5588  dflim2  5923  fun11  6102  feq2  6166  f1eq2  6236  f1eq3  6237  foeq2  6252  brprcneu  6324  ssimaexg  6405  dmfco  6413  fndmdif  6463  respreima  6486  isoeq5  6712  isoini  6729  isopolem  6736  f1oiso  6742  f1oiso2  6743  riotaeqdv  6753  oprabid  6820  oprabv  6848  mpt2eq123  6859  mpt2eq123dva  6861  eloprabga  6892  resoprab  6901  resoprab2  6902  elrnmpt2res  6919  ov  6925  ov3  6942  ov6g  6943  ovg  6944  caoftrn  7077  uniuni  7116  limuni3  7197  elxp4  7255  elxp5  7256  opabex3d  7290  opabex3  7291  opiota  7376  eloprabi  7380  mptmpt2opabbrd  7396  cnvf1o  7425  frxp  7436  xporderlem  7437  poxp  7438  fnwelem  7441  suppimacnv  7455  rexsupp  7462  mpt2curryd  7545  smoel2  7611  omeu  7817  oeeui  7834  omabs  7879  omopth  7890  qliftel  7980  brecop  7990  eroveu  7993  erov  7995  ecopovtrn  8001  ixpsnf1o  8100  dom2lem  8147  mapsnend  8186  xpsnen  8198  xpassen  8208  pw2f1olem  8218  xpf1o  8276  unxpdom  8321  domunfican  8387  preleqALT  8674  preleqOLD  8676  zfinf  8698  cantnfs  8725  tcvalg  8776  r0weon  9033  fseqenlem1  9045  acni2  9067  aceq1  9138  aceq0  9139  dfac2a  9150  dfac12lem2  9166  cardcf  9274  cfeq0  9278  cfsuc  9279  cff1  9280  cfss  9287  isf32lem5  9379  fin1a2lem6  9427  zfac  9482  brdom7disj  9553  brdom6disj  9554  axrepnd  9616  axunndlem1  9617  axinfnd  9628  axacndlem5  9633  axacnd  9634  zfcndrep  9636  zfcndinf  9640  zfcndac  9641  pwfseqlem4a  9683  pwfseqlem4  9684  gruina  9840  grothomex  9851  ordpipq  9964  elnpi  10010  genpass  10031  ltprord  10052  reclem2pr  10070  reclem3pr  10071  recexpr  10073  addsrmo  10094  mulsrmo  10095  addsrpr  10096  mulsrpr  10097  ltsosr  10115  mulgt0sr  10126  supsr  10133  ltresr  10161  axpre-lttrn  10187  axpre-mulgt0  10189  prime  11658  peano5uzti  11667  rexuz  11939  ltxr  12153  qbtwnre  12234  xmulneg1  12303  supxr2  12348  ixxval  12387  fzval  12534  preduz  12668  nn0opth2  13266  hashbclem  13441  hashf1lem2  13445  eqwrd  13546  swrdeq  13656  wrd2ind  13689  cshwcsh2id  13786  eqwrds3  13917  cleq1lem  13934  rtrclreclem3  14011  rtrclreclem4  14012  relexpindlem  14014  abslt  14265  absle  14266  lenegsq  14271  abs2difabs  14285  ello12  14458  elo12  14469  o1lo1  14479  rlimuni  14492  lo1resb  14506  o1resb  14508  2clim  14514  rlimcn2  14532  climcn2  14534  addcn2  14535  mulcn2  14537  o1of2  14554  sumeq1  14630  fsum2dlem  14712  modfsummod  14737  prodeq1f  14849  fprod2dlem  14921  znnenlem  15151  nndivdvds  15203  divalg2  15342  smupval  15424  gcdval  15432  gcdass  15478  lcmval  15519  lcmass  15541  rpexp  15645  pythagtriplem2  15735  pythagtrip  15752  vdwapun  15891  0ram  15937  ramub1lem2  15944  pwsle  16366  imasleval  16415  ismre  16464  ismri  16505  iscatd2  16555  dfiso2  16645  isssc  16693  funcpropd  16773  fullpropd  16793  fthres2b  16803  fthres2c  16804  setcsect  16952  prslem  17145  drsdir  17149  posi  17164  tosso  17250  ipoval  17368  ipolt  17373  odudlatb  17410  dirge  17451  gsumpropd2lem  17487  issgrpv  17500  issgrpn0  17501  mhmpropd  17555  mrcmndind  17580  mgmnsgrpex  17632  issubg3  17826  isga  17937  symgfixelq  18066  psgnfval  18133  psgnval  18140  isslw  18236  dprdw  18623  subgdmdprd  18647  drngpropd  18990  issubrg  18996  islmod  19083  lmodlema  19084  lmodprop2d  19141  lsslss  19180  lbspropd  19318  lbsacsbs  19377  aspval2  19568  psrbag  19585  pf1ind  19940  znleval  20124  islbs4  20394  islinds3  20396  mdetunilem4  20645  mdetunilem9  20650  istopg  20926  basis2  20982  tg2  20996  iscld  21058  neival  21133  isnei  21134  isneip  21136  neiptoptop  21162  neiptopnei  21163  neitr  21211  restlp  21214  iscn  21266  cnpval  21267  iscnp  21268  regsep  21365  1stcclb  21474  2ndc1stc  21481  2ndcctbss  21485  2ndcdisj  21486  llyi  21504  nllyi  21505  hausmapdom  21530  locfinnei  21553  comppfsc  21562  elkgen  21566  txbas  21597  txcls  21634  txcnpi  21638  ptpjopn  21642  txdis1cn  21665  txtube  21670  txcmplem1  21671  hausdiag  21675  tx1stc  21680  txkgen  21682  xkococnlem  21689  xkococn  21690  elqtop  21727  kqreglem1  21771  elmptrab  21857  isfbas  21859  elflim2  21994  elflim  22001  hauspwpwf1  22017  alexsublem  22074  ghmcnp  22144  qustgplem  22150  tsmssubm  22172  elutop  22263  ustuqtop4  22274  isucn  22308  iscfilu  22318  ispsmet  22335  ismet  22354  isxmet  22355  ismet2  22364  imasdsf1olem  22404  blres  22462  elmopn  22473  mopni  22523  neibl  22532  nrmmetd  22605  ngppropd  22667  elcncf  22918  mulc1cncf  22934  elpi1  23070  isclmp  23122  metcld2  23330  pmltpclem1  23442  ovolval  23468  itg1climres  23707  itg2val  23721  isibl  23758  itgeq1f  23764  itgresr  23771  iblcn  23791  itgfsum  23819  dvreslem  23899  dvfsumlem2  24016  deg1ldg  24078  vieta1  24293  ulm2  24365  sincosq2sgn  24478  sincosq4sgn  24480  efopn  24631  dvdsflsumcom  25141  fsumvma2  25166  logfac2  25169  dchrptlem1  25216  lgsdchrval  25306  2lgslem1a  25343  pntibndlem3  25508  pntlemi  25520  pntleme  25524  pnt3  25528  istrkgld  25585  istrkg2ld  25586  istrkg3ld  25587  axtgsegcon  25590  axtg5seg  25591  axtgpasch  25593  axtgupdim2  25597  legov  25707  islnopp  25858  ishpg  25878  iscgra1  25929  brcgr  26007  brbtwn2  26012  axsegconlem1  26024  axsegcon  26034  axcontlem10  26080  edgssv2  26318  uhgr2edg  26328  isfusgrf1  26441  edgnbusgreu  26497  edgnbusgreuOLD  26498  cplgr3v  26572  vtxdun  26618  upgr2wlk  26805  upgrtrls  26839  upgristrl  26840  upgrf1istrl  26841  2pthnloop  26868  usgr2pth  26901  isclwlke  26914  isclwlkupgr  26915  iswwlksnx  26974  wlknewwlksn  27027  wwlksnfi  27055  wspthsnwspthsnonOLD  27067  2pthon3v  27094  elwwlks2on  27111  wpthswwlks2on  27113  wpthswwlks2onOLD  27114  rusgrnumwwlkl1  27121  rusgrnumwwlkb0  27124  clwwlknp  27196  clwwlkel  27206  clwwlkf  27207  erclwwlknsym  27232  erclwwlkntr  27233  clwlksfoclwwlkOLD  27248  clwwlknonelOLD  27274  clwwlknonwwlknonb  27285  clwwlknonwwlknonbOLD  27286  0trl  27306  0spth  27310  0crct  27317  0cycl  27318  upgr4cycl4dv4e  27369  upgriseupth  27391  eupth2lem2  27403  3cyclfrgrrn1  27471  4cycl2vnunb  27476  frgrncvvdeqlem2  27486  frgr2wwlk1  27515  fusgr2wsp2nb  27520  numclwlk1lem1  27562  vciOLD  27757  isvclem  27773  nmoofval  27958  isph  28018  norm3lemt  28350  isch2  28421  cmbr  28784  eigre  29035  eigorth  29038  nmopub  29108  nmfnleub  29125  cvbr  29482  mdbr  29494  dmdbr  29499  chrelat2  29570  mdsymlem2  29604  rexunirn  29671  ifeqeqx  29700  funcnvmptOLD  29808  funcnvmpt  29809  1stpreima  29825  fpwrelmapffslem  29848  isomnd  30042  archirng  30083  isslmd  30096  slmdlema  30097  orngmul  30144  dya2iocuni  30686  omsfval  30697  elcarsg  30708  itgeq12dv  30729  isrrvv  30846  reprinrn  31037  reprdifc  31046  istrkg2d  31085  axtgupdim2OLD  31087  brafs  31091  bnj956  31186  bnj1146  31201  bnj18eq1  31336  kur14  31537  pconncn  31545  cnpconn  31551  txpconn  31553  cvmscbv  31579  cvmcov  31584  cvmsi  31586  cvmsval  31587  cvmopnlem  31599  cvmlift2lem10  31633  cvmlift3lem2  31641  cvmlift3lem6  31645  cvmlift3lem7  31646  cvmlift3lem9  31648  cvmlift3  31649  mclsssvlem  31798  mclsind  31806  eldm3  31990  opelco3  32015  fv1stcnv  32017  fv2ndcnv  32018  dfon2lem6  32030  dfon2lem7  32031  dfon2lem8  32032  dfon2  32034  poseq  32091  soseq  32092  sltval  32138  nolt02o  32183  slelttr  32220  nocvxminlem  32231  elfuns  32360  brsuccf  32386  brofs  32450  5segofs  32451  brifs  32488  ifscgr  32489  brcolinear  32504  lineext  32521  brfs  32524  fscgr  32525  linecgr  32526  btwnconn1lem4  32535  btwnconn1lem8  32539  btwnconn1lem11  32542  btwnconn1lem12  32543  segcon2  32550  brsegle  32553  outsideofeq  32575  funray  32585  funline  32587  fvline  32589  linethru  32598  trer  32648  finminlem  32650  ivthALT  32668  filnetlem4  32714  knoppndvlem21  32861  bj-axrep1  33125  bj-axrep2  33126  bj-axrep3  33127  bj-axsep  33130  bj-ax8  33217  bj-rabeqd  33248  bj-axsep2  33253  bj-zfauscl  33254  csboprabg  33513  topdifinffinlem  33532  icoreval  33538  isbasisrelowllem1  33540  isbasisrelowllem2  33541  relowlssretop  33548  wl-ax11-lem8  33703  curf  33720  ptrest  33741  poimirlem1  33743  poimirlem13  33755  poimirlem14  33756  poimirlem22  33764  poimirlem24  33766  poimirlem26  33768  poimirlem27  33769  heicant  33777  mblfinlem3  33781  mblfinlem4  33782  mbfresfi  33788  itg2addnclem3  33795  itg2addnc  33796  itg2gt0cn  33797  areacirclem5  33836  cover2  33840  cover2g  33841  fdc  33873  fdc1  33874  heibor1  33941  bfp  33955  rngosn3  34055  drngoi  34082  isdrngo1  34087  isriscg  34115  isfldidl2  34200  islshpat  34826  lcvbr  34830  lshpsmreu  34918  ldual1dim  34975  cvrval  35078  cvrnbtwn3  35085  iscvlat2N  35133  ishlat3N  35163  hlrelat5N  35209  3dim0  35265  llnexatN  35329  islpln5  35343  islvol5  35387  pmapjat1  35661  ltrnu  35929  cdleme02N  36031  cdlemg33b  36516  cdlemg33c  36517  dvhb1dimN  36795  dibelval3  36957  dibopelval3  36958  dib1dim  36975  dibglbN  36976  diblsmopel  36981  dicval  36986  dicopelval  36987  dicelval3  36990  dicelval1sta  36997  dihopelvalcpre  37058  dih1dimatlem  37139  dihpN  37146  dihjatcclem4  37231  lpolsetN  37292  mapdpglem3  37485  hdmapglem7a  37737  mrefg2  37796  mzpclval  37814  eldiophb  37846  eldioph2lem1  37849  eldioph3  37855  lzenom  37859  diophin  37862  eldiophss  37864  diophrex  37865  eq0rabdioph  37866  pellexlem3  37921  elpell1qr  37937  elpell14qr  37939  elpell1234qr  37941  jm2.27  38101  rmydioph  38107  expdiophlem1  38114  expdioph  38116  pw2f1ocnv  38130  hbtlem1  38219  hbtlem7  38221  dgraalem  38241  dgraaub  38244  ifpbi2  38337  inintabd  38411  cnvcnvintabd  38432  cnvintabd  38435  clcnvlem  38456  iunrelexpmin1  38526  uneqsn  38847  k0004lem2  38972  binomcxplemnotnn0  39081  2sbc6g  39142  2sbc5g  39143  iotasbc  39146  dropab1  39177  dropab2  39178  cbvmpt21  39800  disjinfi  39901  dmrelrnrel  39938  mullimc  40367  mullimcf  40374  limsuppnfd  40453  limsuppnf  40462  limsupre2  40476  limsupre2mpt  40481  limsupre3  40484  limsupre3mpt  40485  limsupre3uzlem  40486  fourierdlem42  40884  fourierdlem48  40889  fourierdlem50  40891  fourierdlem51  40892  fourierdlem54  40895  fourierdlem86  40927  ovnval2  41280  ovnsubaddlem1  41305  hoiqssbl  41360  vonicclem2  41419  dfdfat2  41732  2ffzoeq  41863  pfxeq  41929  mgmhmpropd  42310  ismhm0  42330  isrnghm  42417  rngcsect  42505  rngcinv  42506  rngcsectALTV  42517  rngcinvALTV  42518  ringcsect  42556  ringcinv  42557  ringcsectALTV  42580  ringcinvALTV  42581  lmod1  42806  elbigo2  42871
  Copyright terms: Public domain W3C validator