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

Theorem anbi1d 629
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 578 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  anbi12d  630  anbi1  631  pm5.71  1023  cador  1602  drsb1  2533  eleq1w  2899  eleq1d  2901  rexeqf  3403  reueq1f  3404  rmoeq1f  3405  reueq1  3412  rmoeq1  3413  rabeqf  3486  rabeqi  3487  rabeq  3488  vtocl2gaf  3580  vtocl4ga  3584  alexeqg  3647  elrabi  3678  reu2eqd  3730  sbc2or  3784  sbc5  3803  rexss  4041  psstr  4084  ineq1OLD  4185  difin2  4269  r19.28z  4445  rexreusng  4615  reurexprg  4638  rabsnifsb  4656  ssunsn2  4758  preq12bg  4782  opeq1  4801  eluni  4839  csbuni  4864  disjxun  5060  mpteq12f  5145  axrep1  5187  axreplem  5188  zfrepclf  5194  axsepgfromrep  5197  axsepg  5200  zfauscl  5201  reusv2lem4  5297  rabxfrd  5313  opthg  5365  otthg  5373  copsexgw  5377  copsexg  5378  opeqsng  5389  euotd  5399  elopab  5410  pocl  5479  xpeq1  5567  elxpi  5575  vtoclr  5613  opbrop  5646  dmopab2rex  5784  resopab2  5902  dflim2  6244  fun11  6424  feq2  6492  f1eq2  6567  f1eq3  6568  foeq2  6583  brprcneu  6658  ssimaexg  6745  dmfco  6753  fndmdif  6807  respreima  6831  isoeq5  7069  isoini  7086  isopolem  7093  f1oiso  7099  f1oiso2  7100  riotaeqdv  7110  oprabidw  7182  oprabid  7183  oprabv  7209  mpoeq123  7221  mpoeq123dva  7223  eloprabga  7254  resoprab  7263  resoprab2  7264  elrnmpores  7281  ov  7287  ov3  7304  ov6g  7305  ovg  7306  caoftrn  7437  uniuni  7476  limuni3  7558  elxp4  7618  elxp5  7619  opabex3d  7660  opabex3rd  7661  opabex3  7662  releldmdifi  7738  opiota  7751  eloprabi  7755  mptmpoopabbrd  7772  cnvf1o  7800  frxp  7814  xporderlem  7815  poxp  7816  fnwelem  7819  suppimacnv  7835  rexsupp  7842  mpocurryd  7929  smoel2  7994  omeu  8204  oeeui  8221  omabs  8267  omopth  8278  qliftel  8373  brecop  8383  eroveu  8385  erov  8387  ecopovtrn  8393  ixpsnf1o  8494  dom2lem  8541  mapsnend  8580  xpsnen  8593  xpassen  8603  pw2f1olem  8613  xpf1o  8671  unxpdom  8717  domunfican  8783  preleqALT  9072  zfinf  9094  cantnfs  9121  tcvalg  9172  r0weon  9430  fseqenlem1  9442  acni2  9464  aceq1  9535  aceq0  9536  dfac2a  9547  dfac12lem2  9562  cardcf  9666  cfeq0  9670  cfsuc  9671  cff1  9672  cfss  9679  isf32lem5  9771  fin1a2lem6  9819  zfac  9874  brdom7disj  9945  brdom6disj  9946  axrepnd  10008  axunndlem1  10009  axinfnd  10020  axacndlem5  10025  axacnd  10026  zfcndrep  10028  zfcndinf  10032  zfcndac  10033  pwfseqlem4a  10075  pwfseqlem4  10076  gruina  10232  grothomex  10243  ordpipq  10356  elnpi  10402  genpass  10423  ltprord  10444  reclem2pr  10462  reclem3pr  10463  recexpr  10465  addsrmo  10487  mulsrmo  10488  addsrpr  10489  mulsrpr  10490  ltsosr  10508  mulgt0sr  10519  supsr  10526  ltresr  10554  axpre-lttrn  10580  axpre-mulgt0  10582  prime  12055  peano5uzti  12064  rexuz  12290  ltxr  12503  qbtwnre  12585  xmulneg1  12655  supxr2  12700  ixxval  12739  fzval  12887  preduz  13022  nn0opth2  13625  hashbclem  13803  hashf1lem2  13807  eqwrd  13902  pfxeq  14051  wrd2ind  14078  cshwcsh2id  14183  eqwrds3  14318  cleq1lem  14335  rtrclreclem3  14412  rtrclreclem4  14413  relexpindlem  14415  abslt  14667  absle  14668  lenegsq  14673  abs2difabs  14687  ello12  14866  elo12  14877  o1lo1  14887  rlimuni  14900  lo1resb  14914  o1resb  14916  2clim  14922  rlimcn2  14940  climcn2  14942  addcn2  14943  mulcn2  14945  o1of2  14962  sumeq1  15038  fsum2dlem  15117  modfsummod  15141  prodeq1f  15254  fprod2dlem  15326  nndivdvds  15608  divalg2  15748  smupval  15829  gcdval  15837  gcdass  15887  lcmval  15928  lcmass  15950  rpexp  16056  pythagtriplem2  16146  pythagtrip  16163  vdwapun  16302  0ram  16348  ramub1lem2  16355  pwsle  16757  imasleval  16806  ismre  16853  ismri  16894  iscatd2  16944  dfiso2  17034  isssc  17082  funcpropd  17162  fullpropd  17182  fthres2b  17192  fthres2c  17193  setcsect  17341  prslem  17533  drsdir  17537  posi  17552  tosso  17638  ipoval  17756  ipolt  17761  odudlatb  17798  dirge  17839  gsumpropd2lem  17880  issgrpv  17894  issgrpn0  17895  mhmpropd  17952  mndind  17977  mgmnsgrpex  18031  issubg3  18229  isga  18353  symgfixelq  18483  psgnfval  18550  psgnval  18557  dprdw  19054  subgdmdprd  19078  drngpropd  19451  issubrg  19457  islmod  19560  lmodlema  19561  lmodprop2d  19618  lsslss  19655  lbspropd  19793  lbsacsbs  19850  aspval2  20048  psrbag  20065  pf1ind  20434  znleval  20617  islbs4  20892  islinds3  20894  mdetunilem4  21140  mdetunilem9  21145  istopg  21419  basis2  21475  tg2  21489  iscld  21551  isnei  21627  isneip  21629  neiptoptop  21655  neiptopnei  21656  neitr  21704  restlp  21707  iscn  21759  cnpval  21760  iscnp  21761  regsep  21858  1stcclb  21968  2ndc1stc  21975  2ndcctbss  21979  2ndcdisj  21980  llyi  21998  nllyi  21999  hausmapdom  22024  locfinnei  22047  comppfsc  22056  elkgen  22060  txbas  22091  txcls  22128  txcnpi  22132  ptpjopn  22136  txdis1cn  22159  txtube  22164  txcmplem1  22165  hausdiag  22169  tx1stc  22174  txkgen  22176  xkococn  22184  elqtop  22221  kqreglem1  22265  elmptrab  22351  isfbas  22353  elflim2  22488  elflim  22495  hauspwpwf1  22511  alexsublem  22568  ghmcnp  22638  qustgplem  22644  tsmssubm  22666  elutop  22757  ustuqtop4  22768  isucn  22802  iscfilu  22812  ispsmet  22829  ismet  22848  isxmet  22849  ismet2  22858  imasdsf1olem  22898  blres  22956  elmopn  22967  mopni  23017  neibl  23026  nrmmetd  23099  ngppropd  23161  elcncf  23412  mulc1cncf  23428  elpi1  23564  isclmp  23616  metcld2  23825  pmltpclem1  23964  itg1climres  24230  itg2val  24244  isibl  24281  itgeq1f  24287  itgresr  24294  iblcn  24314  itgfsum  24342  dvreslem  24422  dvfsumlem2  24539  deg1ldg  24601  vieta1  24816  ulm2  24888  sincosq2sgn  25000  sincosq4sgn  25002  efopn  25154  dvdsflsumcom  25679  fsumvma2  25704  logfac2  25707  dchrptlem1  25754  lgsdchrval  25844  2lgslem1a  25881  pntibndlem3  26082  pntlemi  26094  pntleme  26098  pnt3  26102  istrkgld  26159  istrkg2ld  26160  istrkg3ld  26161  axtgsegcon  26164  axtg5seg  26165  axtgpasch  26167  axtgupdim2  26171  legov  26285  islnopp  26439  ishpg  26459  iscgra1  26510  dfcgra2  26530  dfcgrg2  26563  brcgr  26600  brbtwn2  26605  axsegconlem1  26617  axsegcon  26627  axcontlem10  26673  edgssv2  26894  uhgr2edg  26904  isfusgrf1  27016  edgnbusgreu  27063  cplgr3v  27131  vtxdun  27177  upgr2wlk  27364  upgrtrls  27397  upgristrl  27398  upgrf1istrl  27399  2pthnloop  27426  usgr2pth  27459  isclwlke  27472  isclwlkupgr  27473  iswwlksnx  27532  wlknewwlksn  27579  wwlksnfiOLD  27599  2pthon3v  27636  elwwlks2on  27652  wpthswwlks2on  27654  rusgrnumwwlkl1  27661  rusgrnumwwlkb0  27664  clwwlknp  27729  clwwlkf  27740  erclwwlknsym  27763  erclwwlkntr  27764  clwwlknonwwlknonb  27799  0trl  27815  0spth  27819  0crct  27826  0cycl  27827  upgr4cycl4dv4e  27878  upgriseupth  27900  eupth2lem2  27912  3cyclfrgrrn1  27978  4cycl2vnunb  27983  frgrncvvdeqlem2  27993  frgr2wwlk1  28022  fusgr2wsp2nb  28027  numclwlk1lem1  28062  vciOLD  28252  isvclem  28268  nmoofval  28453  isph  28513  norm3lemt  28843  isch2  28914  cmbr  29275  eigre  29526  eigorth  29529  nmopub  29599  nmfnleub  29616  cvbr  29973  mdbr  29985  dmdbr  29990  chrelat2  30061  mdsymlem2  30095  rexunirn  30170  ifeqeqx  30211  iunrnmptss  30232  funcnvmpt  30327  1stpreima  30355  fpwrelmapffslem  30381  isomnd  30616  archirng  30731  isslmd  30744  slmdlema  30745  orngmul  30790  lindflbs  30854  lindfpropd  30856  ccfldextdgrr  30943  dya2iocuni  31427  omsfval  31438  elcarsg  31449  itgeq12dv  31470  isrrvv  31587  reprinrn  31775  reprdifc  31784  istrkg2d  31823  axtgupdim2ALTV  31825  brafs  31829  bnj956  31934  bnj1146  31949  bnj18eq1  32085  zltp1ne  32232  isacycgr  32276  kur14  32347  pconncn  32355  cnpconn  32361  txpconn  32363  cvmscbv  32389  cvmcov  32394  cvmsi  32396  cvmsval  32397  cvmopnlem  32409  cvmlift2lem10  32443  cvmlift3lem2  32451  cvmlift3lem6  32455  cvmlift3lem7  32456  cvmlift3lem9  32458  cvmlift3  32459  satf0op  32508  sat1el2xp  32510  satffunlem  32532  dmopab3rexdif  32536  mclsssvlem  32693  mclsind  32701  eldm3  32881  opelco3  32902  dfon2lem6  32917  dfon2lem7  32918  dfon2lem8  32919  dfon2  32921  poseq  32979  soseq  32980  sltval  33038  nolt02o  33083  slelttr  33120  nocvxminlem  33131  elfuns  33260  brsuccf  33286  brofs  33350  5segofs  33351  brifs  33388  ifscgr  33389  brcolinear  33404  lineext  33421  brfs  33424  fscgr  33425  linecgr  33426  btwnconn1lem4  33435  btwnconn1lem8  33439  btwnconn1lem11  33442  btwnconn1lem12  33443  segcon2  33450  brsegle  33453  outsideofeq  33475  funray  33485  funline  33487  fvline  33489  linethru  33498  trer  33548  finminlem  33550  ivthALT  33567  filnetlem4  33613  knoppndvlem21  33755  bj-rabeqd  34122  bj-zfauscl  34127  bj-imdirval  34351  csboprabg  34480  topdifinffinlem  34497  icoreval  34503  isbasisrelowllem1  34505  isbasisrelowllem2  34506  relowlssretop  34513  pibp19  34564  wl-ax11-lem8  34691  curf  34737  ptrest  34758  poimirlem1  34760  poimirlem13  34772  poimirlem14  34773  poimirlem22  34781  poimirlem24  34783  poimirlem26  34785  poimirlem27  34786  heicant  34794  mblfinlem3  34798  mblfinlem4  34799  mbfresfi  34805  itg2addnclem3  34812  itg2addnc  34813  itg2gt0cn  34814  areacirclem5  34853  cover2  34857  cover2g  34858  fdc  34888  fdc1  34889  heibor1  34956  bfp  34970  rngosn3  35070  drngoi  35097  isdrngo1  35102  isriscg  35130  isfldidl2  35215  islshpat  36020  lcvbr  36024  lshpsmreu  36112  ldual1dim  36169  cvrval  36272  cvrnbtwn3  36279  iscvlat2N  36327  ishlat3N  36357  hlrelat5N  36404  3dim0  36460  llnexatN  36524  islpln5  36538  islvol5  36582  pmapjat1  36856  ltrnu  37124  cdleme02N  37225  cdlemg33b  37710  cdlemg33c  37711  dvhb1dimN  37989  dibelval3  38150  dibopelval3  38151  dib1dim  38168  dibglbN  38169  diblsmopel  38174  dicval  38179  dicopelval  38180  dicelval3  38183  dicelval1sta  38190  dihopelvalcpre  38251  dih1dimatlem  38332  dihpN  38339  dihjatcclem4  38424  lpolsetN  38485  mapdpglem3  38678  hdmapglem7a  38930  prjspeclsp  39123  mrefg2  39165  mzpclval  39183  eldiophb  39215  eldioph2lem1  39218  eldioph3  39224  lzenom  39228  diophin  39230  eldiophss  39232  diophrex  39233  eq0rabdioph  39234  pellexlem3  39289  elpell1qr  39305  elpell14qr  39307  elpell1234qr  39309  jm2.27  39466  rmydioph  39472  expdiophlem1  39479  expdioph  39481  pw2f1ocnv  39495  hbtlem1  39584  hbtlem7  39586  dgraalem  39606  dgraaub  39609  ifpbi2  39693  inintabd  39800  cnvcnvintabd  39821  cnvintabd  39824  clcnvlem  39844  iunrelexpmin1  39914  uneqsn  40234  k0004lem2  40359  mnuprdlem1  40469  mnuprdlem2  40470  binomcxplemnotnn0  40549  2sbc6g  40608  2sbc5g  40609  iotasbc  40612  dropab1  40640  dropab2  40641  cbvmpo1  41225  disjinfi  41315  dmrelrnrel  41351  mullimc  41758  mullimcf  41765  limsuppnfd  41844  limsuppnf  41853  limsupre2  41867  limsupre2mpt  41872  limsupre3  41875  limsupre3mpt  41876  limsupre3uzlem  41877  fourierdlem42  42296  fourierdlem48  42301  fourierdlem50  42303  fourierdlem51  42304  fourierdlem54  42307  fourierdlem86  42339  ovnval2  42689  ovnsubaddlem1  42714  hoiqssbl  42769  vonicclem2  42828  funressnbrafv2  43305  dfatdmfcoafv2  43315  2ffzoeq  43390  ichreuopeq  43463  prproropf1olem4  43496  prprspr2  43508  prprsprreu  43509  prprreueq  43510  reuopreuprim  43516  mgmhmpropd  43880  ismhm0  43900  isrnghm  43991  rngcsect  44079  rngcinv  44080  rngcsectALTV  44091  rngcinvALTV  44092  ringcsect  44130  ringcinv  44131  ringcsectALTV  44154  ringcinvALTV  44155  lmod1  44375  elbigo2  44440  rrx2vlinest  44556
  Copyright terms: Public domain W3C validator