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

Theorem anbi1d 633
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
anbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
anbi1d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))

Proof of Theorem anbi1d
StepHypRef Expression
1 anbid.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 25 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
32pm5.32rd 581 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  anbi12d  634  anbi1  635  pm5.71  1028  cador  1615  drsb1  2500  eleq1w  2822  eleq1d  2824  clelab  2882  rexeqf  3324  reueq1f  3325  rmoeq1f  3326  reueq1  3335  rmoeq1  3336  rabeqf  3405  rabeqiOLD  3407  rabeq  3408  cgsex4g  3466  vtocl2gaf  3505  vtocl4ga  3510  alexeqg  3572  elrabiOLD  3611  reu2eqd  3665  sbc2or  3719  sbc5ALT  3739  rexss  3988  psstr  4035  difin2  4222  r19.28z  4425  dfif6  4458  rexreusng  4611  reurexprg  4636  rabsnifsb  4654  ssunsn2  4756  preq12bg  4780  opeq1  4800  eluni  4838  csbuni  4866  disjxun  5067  unopab  5150  mpteq12f  5154  axrep1  5196  axreplem  5197  zfrepclf  5203  axsepgfromrep  5206  axsepg  5209  zfauscl  5210  reusv2lem4  5310  rabxfrd  5326  opthg  5377  otthg  5385  copsexgw  5389  copsexg  5390  opeqsng  5402  euotd  5412  elopab  5424  pocl  5492  poclOLD  5493  xpeq1  5582  elxpi  5590  vtoclr  5629  opbrop  5662  dmopab2rex  5803  resopab2  5921  dflim2  6289  fun11  6474  feq2  6548  f1eq2  6632  f1eq3  6633  foeq2  6651  brprcneu  6729  fvprc  6730  ssimaexg  6818  dmfco  6828  fndmdif  6883  respreima  6907  isoeq5  7151  isoini  7168  isopolem  7175  f1oiso  7181  f1oiso2  7182  riotaeqdv  7192  oprabidw  7265  oprabid  7266  oprabv  7292  mpoeq123  7304  mpoeq123dva  7306  0mpo0  7315  eloprabga  7339  eloprabgaOLD  7340  resoprab  7349  resoprab2  7350  elrnmpores  7368  ov  7374  ov3  7392  ov6g  7393  ovg  7394  caoftrn  7527  uniuni  7568  limuni3  7652  elxp4  7721  elxp5  7722  opabex3d  7759  opabex3rd  7760  opabex3  7761  releldmdifi  7837  opiota  7850  eloprabi  7854  mptmpoopabbrd  7872  cnvf1o  7900  frxp  7916  xporderlem  7917  poxp  7918  fnwelem  7921  suppimacnv  7939  rexsupp  7947  mpocurryd  8034  smoel2  8123  omeu  8336  oeeui  8353  omabs  8399  omopth  8410  qliftel  8505  brecop  8515  eroveu  8517  erov  8519  ecopovtrn  8525  ixpsnf1o  8642  dom2lem  8693  mapsnend  8738  xpsnen  8754  xpassen  8764  pw2f1olem  8774  xpf1o  8833  unxpdom  8912  domunfican  8971  preleqALT  9259  zfinf  9281  cantnfs  9308  tcvalg  9381  r0weon  9653  fseqenlem1  9665  acni2  9687  aceq1  9758  aceq0  9759  dfac2a  9770  dfac12lem2  9785  cardcf  9893  cfeq0  9897  cfsuc  9898  cff1  9899  cfss  9906  isf32lem5  9998  fin1a2lem6  10046  zfac  10101  brdom7disj  10172  brdom6disj  10173  axrepnd  10235  axunndlem1  10236  axinfnd  10247  axacndlem5  10252  axacnd  10253  zfcndrep  10255  zfcndinf  10259  zfcndac  10260  pwfseqlem4a  10302  pwfseqlem4  10303  gruina  10459  grothomex  10470  ordpipq  10583  elnpi  10629  genpass  10650  ltprord  10671  reclem2pr  10689  reclem3pr  10690  recexpr  10692  addsrmo  10714  mulsrmo  10715  addsrpr  10716  mulsrpr  10717  ltsosr  10735  mulgt0sr  10746  supsr  10753  ltresr  10781  axpre-lttrn  10807  axpre-mulgt0  10809  prime  12285  peano5uzti  12294  rexuz  12521  ltxr  12734  qbtwnre  12816  xmulneg1  12886  supxr2  12931  ixxval  12970  fzval  13124  preduz  13261  nn0opth2  13868  hashbclem  14046  hashf1lem2  14052  eqwrd  14142  pfxeq  14291  wrd2ind  14318  cshwcsh2id  14423  eqwrds3  14558  cleq1lem  14575  rtrclreclem3  14653  rtrclreclem4  14654  relexpindlem  14656  abslt  14908  absle  14909  lenegsq  14914  abs2difabs  14928  ello12  15107  elo12  15118  o1lo1  15128  rlimuni  15141  lo1resb  15155  o1resb  15157  2clim  15163  rlimcn3  15181  climcn2  15184  addcn2  15185  mulcn2  15187  o1of2  15204  sumeq1  15282  fsum2dlem  15364  modfsummod  15388  prodeq1f  15500  fprod2dlem  15572  nndivdvds  15854  divalg2  15996  smupval  16077  gcdval  16085  gcdass  16137  lcmval  16179  lcmass  16201  rpexp  16309  pythagtriplem2  16400  pythagtrip  16417  vdwapun  16557  0ram  16603  ramub1lem2  16610  pwsle  17027  imasleval  17076  ismre  17123  ismri  17164  iscatd2  17214  dfiso2  17307  isssc  17355  funcpropd  17437  fullpropd  17457  fthres2b  17467  fthres2c  17468  setcsect  17625  cat1lem  17632  cat1  17633  prslem  17835  drsdir  17839  posi  17854  tosso  17955  odudlatb  18061  ipoval  18066  ipolt  18071  dirge  18139  gsumpropd2lem  18181  issgrpv  18195  issgrpn0  18196  mhmpropd  18254  mndind  18284  mgmnsgrpex  18388  issubg3  18591  isga  18715  symgfixelq  18855  psgnfval  18922  psgnval  18929  dprdw  19427  subgdmdprd  19451  drngpropd  19824  issubrg  19830  islmod  19933  lmodlema  19934  lmodprop2d  19991  lsslss  20028  lbspropd  20166  lbsacsbs  20223  znleval  20549  islbs4  20824  islinds3  20826  aspval2  20887  psrbag  20905  pf1ind  21300  mdetunilem4  21541  mdetunilem9  21546  istopg  21821  basis2  21877  tg2  21891  iscld  21953  isnei  22029  isneip  22031  neiptoptop  22057  neiptopnei  22058  neitr  22106  restlp  22109  iscn  22161  cnpval  22162  iscnp  22163  regsep  22260  1stcclb  22370  2ndc1stc  22377  2ndcctbss  22381  2ndcdisj  22382  llyi  22400  nllyi  22401  hausmapdom  22426  locfinnei  22449  comppfsc  22458  elkgen  22462  txbas  22493  txcls  22530  txcnpi  22534  ptpjopn  22538  txdis1cn  22561  txtube  22566  txcmplem1  22567  hausdiag  22571  tx1stc  22576  txkgen  22578  xkococn  22586  elqtop  22623  kqreglem1  22667  elmptrab  22753  isfbas  22755  elflim2  22890  elflim  22897  hauspwpwf1  22913  alexsublem  22970  ghmcnp  23041  qustgplem  23047  tsmssubm  23069  elutop  23160  ustuqtop4  23171  isucn  23204  iscfilu  23214  ispsmet  23231  ismet  23250  isxmet  23251  ismet2  23260  imasdsf1olem  23300  blres  23358  elmopn  23369  mopni  23419  neibl  23428  nrmmetd  23501  ngppropd  23564  elcncf  23815  mulc1cncf  23831  elpi1  23971  isclmp  24023  metcld2  24233  pmltpclem1  24374  itg1climres  24641  itg2val  24655  isibl  24692  itgeq1f  24698  itgresr  24705  iblcn  24725  itgfsum  24753  dvreslem  24835  dvfsumlem2  24953  deg1ldg  25019  vieta1  25234  ulm2  25306  sincosq2sgn  25418  sincosq4sgn  25420  efopn  25575  dvdsflsumcom  26099  fsumvma2  26124  logfac2  26127  dchrptlem1  26174  lgsdchrval  26264  2lgslem1a  26301  pntibndlem3  26502  pntlemi  26514  pntleme  26518  pnt3  26522  istrkgld  26579  istrkg2ld  26580  istrkg3ld  26581  axtgsegcon  26584  axtg5seg  26585  axtgpasch  26587  axtgupdim2  26591  legov  26705  islnopp  26859  ishpg  26879  iscgra1  26930  dfcgra2  26950  dfcgrg2  26983  brcgr  27020  brbtwn2  27025  axsegconlem1  27037  axsegcon  27047  axcontlem10  27093  edgssv2  27315  uhgr2edg  27325  isfusgrf1  27437  edgnbusgreu  27484  cplgr3v  27552  vtxdun  27598  upgr2wlk  27785  upgrtrls  27818  upgristrl  27819  upgrf1istrl  27820  2pthnloop  27847  usgr2pth  27880  isclwlke  27893  isclwlkupgr  27894  iswwlksnx  27953  wlknewwlksn  28000  2pthon3v  28056  elwwlks2on  28072  wpthswwlks2on  28074  rusgrnumwwlkl1  28081  rusgrnumwwlkb0  28084  clwwlknp  28149  clwwlkf  28159  erclwwlknsym  28182  erclwwlkntr  28183  clwwlknonwwlknonb  28218  0trl  28234  0spth  28238  0crct  28245  0cycl  28246  upgr4cycl4dv4e  28297  upgriseupth  28319  eupth2lem2  28331  3cyclfrgrrn1  28397  4cycl2vnunb  28402  frgrncvvdeqlem2  28412  frgr2wwlk1  28441  fusgr2wsp2nb  28446  numclwlk1lem1  28481  vciOLD  28671  isvclem  28687  nmoofval  28872  isph  28932  norm3lemt  29262  isch2  29333  cmbr  29694  eigre  29945  eigorth  29948  nmopub  30018  nmfnleub  30035  cvbr  30392  mdbr  30404  dmdbr  30409  chrelat2  30480  mdsymlem2  30514  rexunirn  30588  ifeqeqx  30633  iunrnmptss  30653  funcnvmpt  30753  ressupprn  30773  1stpreima  30788  fpwrelmapffslem  30816  isomnd  31075  archirng  31190  isslmd  31203  slmdlema  31204  orngmul  31250  lindflbs  31317  lindfpropd  31319  idlsrgval  31391  ccfldextdgrr  31485  dya2iocuni  31991  omsfval  32002  elcarsg  32013  itgeq12dv  32034  isrrvv  32151  reprinrn  32339  reprdifc  32348  istrkg2d  32387  axtgupdim2ALTV  32389  brafs  32393  bnj956  32497  bnj1146  32512  bnj18eq1  32648  zltp1ne  32809  isacycgr  32848  kur14  32919  pconncn  32927  cnpconn  32933  txpconn  32935  cvmscbv  32961  cvmcov  32966  cvmsi  32968  cvmsval  32969  cvmopnlem  32981  cvmlift2lem10  33015  cvmlift3lem2  33023  cvmlift3lem6  33027  cvmlift3lem7  33028  cvmlift3lem9  33030  cvmlift3  33031  satf0op  33080  sat1el2xp  33082  satffunlem  33104  dmopab3rexdif  33108  mclsssvlem  33265  mclsind  33273  imaeqsexv  33434  eldifsucnn  33438  eldm3  33475  opelco3  33496  dfon2lem6  33511  dfon2lem7  33512  dfon2lem8  33513  dfon2  33515  brttrcl  33540  ttrclselem2  33553  poxp2  33558  xpord3pred  33566  poseq  33570  soseq  33571  sltval  33618  nolt02o  33666  slelttr  33728  nocvxminlem  33740  madebday  33848  sltlpss  33855  elfuns  33985  brsuccf  34011  brofs  34075  5segofs  34076  brifs  34113  ifscgr  34114  brcolinear  34129  lineext  34146  brfs  34149  fscgr  34150  linecgr  34151  btwnconn1lem4  34160  btwnconn1lem8  34164  btwnconn1lem11  34167  btwnconn1lem12  34168  segcon2  34175  brsegle  34178  outsideofeq  34200  funray  34210  funline  34212  fvline  34214  linethru  34223  trer  34273  finminlem  34275  ivthALT  34292  filnetlem4  34338  knoppndvlem21  34480  bj-rabeqd  34875  bj-zfauscl  34880  bj-elgab  34895  bj-imdirvallem  35118  csboprabg  35270  topdifinffinlem  35287  icoreval  35293  isbasisrelowllem1  35295  isbasisrelowllem2  35296  relowlssretop  35303  pibp19  35354  wl-ax11-lem8  35512  curf  35524  ptrest  35545  poimirlem1  35547  poimirlem13  35559  poimirlem14  35560  poimirlem22  35568  poimirlem24  35570  poimirlem26  35572  poimirlem27  35573  heicant  35581  mblfinlem3  35585  mblfinlem4  35586  mbfresfi  35592  itg2addnclem3  35599  itg2addnc  35600  itg2gt0cn  35601  areacirclem5  35638  cover2  35641  cover2g  35642  fdc  35672  fdc1  35673  heibor1  35737  bfp  35751  rngosn3  35851  drngoi  35878  isdrngo1  35883  isriscg  35911  isfldidl2  35996  islshpat  36800  lcvbr  36804  lshpsmreu  36892  ldual1dim  36949  cvrval  37052  cvrnbtwn3  37059  iscvlat2N  37107  ishlat3N  37137  hlrelat5N  37184  3dim0  37240  llnexatN  37304  islpln5  37318  islvol5  37362  pmapjat1  37636  ltrnu  37904  cdleme02N  38005  cdlemg33b  38490  cdlemg33c  38491  dvhb1dimN  38769  dibelval3  38930  dibopelval3  38931  dib1dim  38948  dibglbN  38949  diblsmopel  38954  dicval  38959  dicopelval  38960  dicelval3  38963  dicelval1sta  38970  dihopelvalcpre  39031  dih1dimatlem  39112  dihpN  39119  dihjatcclem4  39204  lpolsetN  39265  mapdpglem3  39458  hdmapglem7a  39710  fsuppind  40025  fsuppssindlem2  40027  prjspeclsp  40194  mrefg2  40267  mzpclval  40285  eldiophb  40317  eldioph2lem1  40320  eldioph3  40326  lzenom  40330  diophin  40332  eldiophss  40334  diophrex  40335  eq0rabdioph  40336  pellexlem3  40391  elpell1qr  40407  elpell14qr  40409  elpell1234qr  40411  jm2.27  40568  rmydioph  40574  expdiophlem1  40581  expdioph  40583  pw2f1ocnv  40597  hbtlem1  40686  hbtlem7  40688  dgraalem  40708  dgraaub  40711  ifpbi2  40794  inintabd  40898  cnvcnvintabd  40919  cnvintabd  40922  clcnvlem  40942  iunrelexpmin1  41028  uneqsn  41345  k0004lem2  41470  mnuprdlem1  41598  mnuprdlem2  41599  binomcxplemnotnn0  41682  2sbc6g  41741  2sbc5g  41742  iotasbc  41745  dropab1  41773  dropab2  41774  cbvmpo1  42356  disjinfi  42439  dmrelrnrel  42473  mullimc  42865  mullimcf  42872  limsuppnfd  42951  limsuppnf  42960  limsupre2  42974  limsupre2mpt  42979  limsupre3  42982  limsupre3mpt  42983  limsupre3uzlem  42984  fourierdlem42  43398  fourierdlem48  43403  fourierdlem50  43405  fourierdlem51  43406  fourierdlem54  43409  fourierdlem86  43441  ovnval2  43791  ovnsubaddlem1  43816  hoiqssbl  43871  vonicclem2  43930  f1cof1b  44274  f1ocof1ob2  44279  funressnbrafv2  44441  dfatdmfcoafv2  44451  2ffzoeq  44526  fundcmpsurbijinj  44568  ichreuopeq  44631  prproropf1olem4  44664  prprspr2  44676  prprsprreu  44677  prprreueq  44678  reuopreuprim  44684  mgmhmpropd  45045  ismhm0  45065  isrnghm  45156  rngcsect  45244  rngcinv  45245  rngcsectALTV  45256  rngcinvALTV  45257  ringcsect  45295  ringcinv  45296  ringcsectALTV  45319  ringcinvALTV  45320  lmod1  45539  elbigo2  45604  rrx2vlinest  45793  i0oii  45919  io1ii  45920  lubeldm2d  45958  glbeldm2d  45959  functhinc  46032  fullthinc  46033
  Copyright terms: Public domain W3C validator