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

Theorem anbi1d 617
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 569 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  anbi12d  618  anbi1  619  bi2anan9  622  pm5.71  1043  cador  1702  drsb1  2536  eleq1w  2868  eleq1d  2870  rexeqf  3324  reueq1f  3325  rmoeq1f  3326  rabeqf  3380  vtocl2gaf  3466  vtocl4ga  3471  alexeqg  3526  elrabi  3554  reu2eqd  3601  sbc2or  3642  sbc5  3658  rexss  3866  psstr  3909  ineq1  4006  difin2  4091  r19.28z  4258  rabsnifsb  4448  ssunsn2  4548  preq12bg  4573  prel12gOLD  4574  opeq1  4595  eluni  4633  csbuni  4660  disjxun  4842  mpteq12f  4925  axrep1  4965  axreplem  4966  zfrepclf  4971  axsep  4974  axsep2  4976  zfauscl  4977  reusv2lem4  5070  rabxfrd  5086  opthg  5135  otthg  5143  copsexg  5145  opeqsng  5156  euotd  5168  elopab  5178  pocl  5239  xpeq1  5325  elxpi  5332  vtoclr  5364  opbrop  5400  opelresgOLD  5609  resopab2  5653  dflim2  5994  fun11  6174  feq2  6238  f1eq2  6312  f1eq3  6313  foeq2  6328  brprcneu  6400  ssimaexg  6485  dmfco  6493  fndmdif  6543  respreima  6566  isoeq5  6795  isoini  6812  isopolem  6819  f1oiso  6825  f1oiso2  6826  riotaeqdv  6836  oprabid  6905  oprabv  6933  mpt2eq123  6944  mpt2eq123dva  6946  eloprabga  6977  resoprab  6986  resoprab2  6987  elrnmpt2res  7004  ov  7010  ov3  7027  ov6g  7028  ovg  7029  caoftrn  7162  uniuni  7201  limuni3  7282  elxp4  7340  elxp5  7341  opabex3d  7375  opabex3  7376  opiota  7461  eloprabi  7465  mptmpt2opabbrd  7481  cnvf1o  7510  frxp  7521  xporderlem  7522  poxp  7523  fnwelem  7526  suppimacnv  7540  rexsupp  7547  mpt2curryd  7630  smoel2  7696  omeu  7902  oeeui  7919  omabs  7964  omopth  7975  qliftel  8065  brecop  8075  eroveu  8078  erov  8080  ecopovtrn  8086  ixpsnf1o  8185  dom2lem  8232  mapsnend  8271  xpsnen  8283  xpassen  8293  pw2f1olem  8303  xpf1o  8361  unxpdom  8406  domunfican  8472  preleqALT  8759  preleqOLD  8761  zfinf  8783  cantnfs  8810  tcvalg  8861  r0weon  9118  fseqenlem1  9130  acni2  9152  aceq1  9223  aceq0  9224  dfac2a  9235  dfac12lem2  9251  cardcf  9359  cfeq0  9363  cfsuc  9364  cff1  9365  cfss  9372  isf32lem5  9464  fin1a2lem6  9512  zfac  9567  brdom7disj  9638  brdom6disj  9639  axrepnd  9701  axunndlem1  9702  axinfnd  9713  axacndlem5  9718  axacnd  9719  zfcndrep  9721  zfcndinf  9725  zfcndac  9726  pwfseqlem4a  9768  pwfseqlem4  9769  gruina  9925  grothomex  9936  ordpipq  10049  elnpi  10095  genpass  10116  ltprord  10137  reclem2pr  10155  reclem3pr  10156  recexpr  10158  addsrmo  10179  mulsrmo  10180  addsrpr  10181  mulsrpr  10182  ltsosr  10200  mulgt0sr  10211  supsr  10218  ltresr  10246  axpre-lttrn  10272  axpre-mulgt0  10274  prime  11724  peano5uzti  11733  rexuz  11956  ltxr  12165  qbtwnre  12248  xmulneg1  12317  supxr2  12362  ixxval  12401  fzval  12551  preduz  12685  nn0opth2  13279  hashbclem  13453  hashf1lem2  13457  eqwrd  13558  swrdeq  13668  wrd2ind  13701  cshwcsh2id  13798  eqwrds3  13929  cleq1lem  13946  rtrclreclem3  14023  rtrclreclem4  14024  relexpindlem  14026  abslt  14277  absle  14278  lenegsq  14283  abs2difabs  14297  ello12  14470  elo12  14481  o1lo1  14491  rlimuni  14504  lo1resb  14518  o1resb  14520  2clim  14526  rlimcn2  14544  climcn2  14546  addcn2  14547  mulcn2  14549  o1of2  14566  sumeq1  14642  fsum2dlem  14724  modfsummod  14748  prodeq1f  14859  fprod2dlem  14931  znnenlemOLD  15160  nndivdvds  15212  divalg2  15348  smupval  15429  gcdval  15437  gcdass  15483  lcmval  15524  lcmass  15546  rpexp  15649  pythagtriplem2  15739  pythagtrip  15756  vdwapun  15895  0ram  15941  ramub1lem2  15948  pwsle  16357  imasleval  16406  ismre  16455  ismri  16496  iscatd2  16546  dfiso2  16636  isssc  16684  funcpropd  16764  fullpropd  16784  fthres2b  16794  fthres2c  16795  setcsect  16943  prslem  17136  drsdir  17140  posi  17155  tosso  17241  ipoval  17359  ipolt  17364  odudlatb  17401  dirge  17442  gsumpropd2lem  17478  issgrpv  17491  issgrpn0  17492  mhmpropd  17546  mrcmndind  17571  mgmnsgrpex  17623  issubg3  17814  isga  17925  symgfixelq  18054  psgnfval  18121  psgnval  18128  isslw  18224  dprdw  18611  subgdmdprd  18635  drngpropd  18978  issubrg  18984  islmod  19071  lmodlema  19072  lmodprop2d  19129  lsslss  19168  lbspropd  19306  lbsacsbs  19365  aspval2  19556  psrbag  19573  pf1ind  19927  znleval  20110  islbs4  20381  islinds3  20383  mdetunilem4  20632  mdetunilem9  20637  istopg  20913  basis2  20969  tg2  20983  iscld  21045  neival  21120  isnei  21121  isneip  21123  neiptoptop  21149  neiptopnei  21150  neitr  21198  restlp  21201  iscn  21253  cnpval  21254  iscnp  21255  regsep  21352  1stcclb  21461  2ndc1stc  21468  2ndcctbss  21472  2ndcdisj  21473  llyi  21491  nllyi  21492  hausmapdom  21517  locfinnei  21540  comppfsc  21549  elkgen  21553  txbas  21584  txcls  21621  txcnpi  21625  ptpjopn  21629  txdis1cn  21652  txtube  21657  txcmplem1  21658  hausdiag  21662  tx1stc  21667  txkgen  21669  xkococnlem  21676  xkococn  21677  elqtop  21714  kqreglem1  21758  elmptrab  21844  isfbas  21846  elflim2  21981  elflim  21988  hauspwpwf1  22004  alexsublem  22061  ghmcnp  22131  qustgplem  22137  tsmssubm  22159  elutop  22250  ustuqtop4  22261  isucn  22295  iscfilu  22305  ispsmet  22322  ismet  22341  isxmet  22342  ismet2  22351  imasdsf1olem  22391  blres  22449  elmopn  22460  mopni  22510  neibl  22519  nrmmetd  22592  ngppropd  22654  elcncf  22905  mulc1cncf  22921  elpi1  23057  isclmp  23109  metcld2  23317  pmltpclem1  23429  ovolval  23454  itg1climres  23695  itg2val  23709  isibl  23746  itgeq1f  23752  itgresr  23759  iblcn  23779  itgfsum  23807  dvreslem  23887  dvfsumlem2  24004  deg1ldg  24066  vieta1  24281  ulm2  24353  sincosq2sgn  24466  sincosq4sgn  24468  efopn  24618  dvdsflsumcom  25128  fsumvma2  25153  logfac2  25156  dchrptlem1  25203  lgsdchrval  25293  2lgslem1a  25330  pntibndlem3  25495  pntlemi  25507  pntleme  25511  pnt3  25515  istrkgld  25572  istrkg2ld  25573  istrkg3ld  25574  axtgsegcon  25577  axtg5seg  25578  axtgpasch  25580  axtgupdim2  25584  legov  25694  islnopp  25845  ishpg  25865  iscgra1  25916  brcgr  25994  brbtwn2  25999  axsegconlem1  26011  axsegcon  26021  axcontlem10  26067  edgssv2  26305  uhgr2edg  26315  isfusgrf1  26428  edgnbusgreu  26484  edgnbusgreuOLD  26485  cplgr3v  26559  vtxdun  26605  upgr2wlk  26792  upgrtrls  26826  upgristrl  26827  upgrf1istrl  26828  2pthnloop  26855  usgr2pth  26888  isclwlke  26901  isclwlkupgr  26902  iswwlksnx  26961  wlknewwlksn  27014  wwlksnfi  27043  wspthsnwspthsnonOLD  27056  2pthon3v  27083  elwwlks2on  27100  wpthswwlks2on  27102  wpthswwlks2onOLD  27103  rusgrnumwwlkl1  27110  rusgrnumwwlkb0  27113  clwwlknp  27185  clwwlkel  27195  clwwlkf  27196  erclwwlknsym  27221  erclwwlkntr  27222  clwlksfoclwwlkOLD  27237  clwwlknonelOLD  27263  clwwlknonwwlknonb  27274  clwwlknonwwlknonbOLD  27275  0trl  27295  0spth  27299  0crct  27306  0cycl  27307  upgr4cycl4dv4e  27358  upgriseupth  27380  eupth2lem2  27392  3cyclfrgrrn1  27460  4cycl2vnunb  27465  frgrncvvdeqlem2  27475  frgr2wwlk1  27504  fusgr2wsp2nb  27509  numclwlk1lem1  27549  vciOLD  27744  isvclem  27760  nmoofval  27945  isph  28005  norm3lemt  28337  isch2  28408  cmbr  28771  eigre  29022  eigorth  29025  nmopub  29095  nmfnleub  29112  cvbr  29469  mdbr  29481  dmdbr  29486  chrelat2  29557  mdsymlem2  29591  rexunirn  29657  ifeqeqx  29686  funcnvmptOLD  29794  funcnvmpt  29795  1stpreima  29811  fpwrelmapffslem  29834  isomnd  30026  archirng  30067  isslmd  30080  slmdlema  30081  orngmul  30128  dya2iocuni  30670  omsfval  30681  elcarsg  30692  itgeq12dv  30713  isrrvv  30830  reprinrn  31021  reprdifc  31030  istrkg2d  31069  axtgupdim2OLD  31071  brafs  31075  bnj956  31170  bnj1146  31185  bnj18eq1  31320  kur14  31521  pconncn  31529  cnpconn  31535  txpconn  31537  cvmscbv  31563  cvmcov  31568  cvmsi  31570  cvmsval  31571  cvmopnlem  31583  cvmlift2lem10  31617  cvmlift3lem2  31625  cvmlift3lem6  31629  cvmlift3lem7  31630  cvmlift3lem9  31632  cvmlift3  31633  mclsssvlem  31782  mclsind  31790  eldm3  31973  opelco3  31998  fv1stcnv  32000  fv2ndcnv  32001  dfon2lem6  32013  dfon2lem7  32014  dfon2lem8  32015  dfon2  32017  poseq  32074  soseq  32075  sltval  32121  nolt02o  32166  slelttr  32203  nocvxminlem  32214  elfuns  32343  brsuccf  32369  brofs  32433  5segofs  32434  brifs  32471  ifscgr  32472  brcolinear  32487  lineext  32504  brfs  32507  fscgr  32508  linecgr  32509  btwnconn1lem4  32518  btwnconn1lem8  32522  btwnconn1lem11  32525  btwnconn1lem12  32526  segcon2  32533  brsegle  32536  outsideofeq  32558  funray  32568  funline  32570  fvline  32572  linethru  32581  trer  32631  finminlem  32633  ivthALT  32651  filnetlem4  32697  knoppndvlem21  32840  bj-axrep1  33102  bj-axrep2  33103  bj-axrep3  33104  bj-axsep  33107  bj-ax8  33195  bj-rabeqd  33226  bj-axsep2  33231  bj-zfauscl  33232  csboprabg  33493  topdifinffinlem  33511  icoreval  33517  isbasisrelowllem1  33519  isbasisrelowllem2  33520  relowlssretop  33527  wl-ax11-lem8  33683  curf  33700  ptrest  33721  poimirlem1  33723  poimirlem13  33735  poimirlem14  33736  poimirlem22  33744  poimirlem24  33746  poimirlem26  33748  poimirlem27  33749  heicant  33757  mblfinlem3  33761  mblfinlem4  33762  mbfresfi  33768  itg2addnclem3  33775  itg2addnc  33776  itg2gt0cn  33777  areacirclem5  33816  cover2  33820  cover2g  33821  fdc  33852  fdc1  33853  heibor1  33920  bfp  33934  rngosn3  34034  drngoi  34061  isdrngo1  34066  isriscg  34094  isfldidl2  34179  islshpat  34797  lcvbr  34801  lshpsmreu  34889  ldual1dim  34946  cvrval  35049  cvrnbtwn3  35056  iscvlat2N  35104  ishlat3N  35134  hlrelat5N  35181  3dim0  35237  llnexatN  35301  islpln5  35315  islvol5  35359  pmapjat1  35633  ltrnu  35901  cdleme02N  36003  cdlemg33b  36488  cdlemg33c  36489  dvhb1dimN  36767  dibelval3  36928  dibopelval3  36929  dib1dim  36946  dibglbN  36947  diblsmopel  36952  dicval  36957  dicopelval  36958  dicelval3  36961  dicelval1sta  36968  dihopelvalcpre  37029  dih1dimatlem  37110  dihpN  37117  dihjatcclem4  37202  lpolsetN  37263  mapdpglem3  37456  hdmapglem7a  37708  mrefg2  37772  mzpclval  37790  eldiophb  37822  eldioph2lem1  37825  eldioph3  37831  lzenom  37835  diophin  37838  eldiophss  37840  diophrex  37841  eq0rabdioph  37842  pellexlem3  37897  elpell1qr  37913  elpell14qr  37915  elpell1234qr  37917  jm2.27  38076  rmydioph  38082  expdiophlem1  38089  expdioph  38091  pw2f1ocnv  38105  hbtlem1  38194  hbtlem7  38196  dgraalem  38216  dgraaub  38219  ifpbi2  38311  inintabd  38385  cnvcnvintabd  38406  cnvintabd  38409  clcnvlem  38430  iunrelexpmin1  38500  uneqsn  38821  k0004lem2  38946  binomcxplemnotnn0  39055  2sbc6g  39115  2sbc5g  39116  iotasbc  39119  dropab1  39149  dropab2  39150  cbvmpt21  39771  disjinfi  39869  dmrelrnrel  39906  mullimc  40328  mullimcf  40335  limsuppnfd  40414  limsuppnf  40423  limsupre2  40437  limsupre2mpt  40442  limsupre3  40445  limsupre3mpt  40446  limsupre3uzlem  40447  fourierdlem42  40845  fourierdlem48  40850  fourierdlem50  40852  fourierdlem51  40853  fourierdlem54  40856  fourierdlem86  40888  ovnval2  41241  ovnsubaddlem1  41266  hoiqssbl  41321  vonicclem2  41380  dfdfat2  41717  funressnbrafv2  41833  dfatdmfcoafv2  41843  2ffzoeq  41913  pfxeq  41979  mgmhmpropd  42353  ismhm0  42373  isrnghm  42460  rngcsect  42548  rngcinv  42549  rngcsectALTV  42560  rngcinvALTV  42561  ringcsect  42599  ringcinv  42600  ringcsectALTV  42623  ringcinvALTV  42624  lmod1  42849  elbigo2  42914
  Copyright terms: Public domain W3C validator