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 671 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 386
This theorem is referenced by:  anbi1  742  anbi12d  746  bi2anan9  916  pm5.71  976  cador  1545  drsb1  2375  eleq1w  2682  eleq1d  2684  rexeqf  3130  reueq1f  3131  rmoeq1f  3132  rabeqf  3185  vtocl2gaf  3268  vtocl4ga  3273  alexeqg  3326  elrabi  3353  reu2eqd  3397  sbc2or  3438  sbc5  3454  rexss  3661  psstr  3703  ineq1  3799  difin2  3882  r19.28z  4054  rabsnifsb  4248  ssunsn2  4350  preq12bg  4377  prel12g  4378  opeq1  4393  eluni  4430  csbuni  4457  disjxun  4642  mpteq12f  4722  axrep1  4763  axrep2  4764  axrep3  4765  zfrepclf  4768  axsep  4771  axsep2  4773  zfauscl  4774  reusv2lem4  4863  rabxfrd  4880  opthg  4936  otthg  4944  copsexg  4946  euotd  4965  elopab  4973  pocl  5032  xpeq1  5118  elxpi  5120  vtoclr  5154  opbrop  5188  opelresg  5392  resopab2  5436  dflim2  5769  fun11  5951  feq2  6014  f1eq2  6084  f1eq3  6085  foeq2  6099  brprcneu  6171  ssimaexg  6251  dmfco  6259  fndmdif  6307  respreima  6330  isoeq5  6556  isoini  6573  isopolem  6580  f1oiso  6586  f1oiso2  6587  riotaeqdv  6597  oprabid  6662  oprabv  6688  mpt2eq123  6699  mpt2eq123dva  6701  eloprabga  6732  resoprab  6741  resoprab2  6742  elrnmpt2res  6759  ov  6765  ov3  6782  ov6g  6783  ovg  6784  caoftrn  6917  uniuni  6956  limuni3  7037  elxp4  7095  elxp5  7096  opabex3d  7130  opabex3  7131  opiota  7214  eloprabi  7217  mptmpt2opabbrd  7233  cnvf1o  7261  frxp  7272  xporderlem  7273  poxp  7274  fnwelem  7277  suppimacnv  7291  rexsupp  7298  mpt2curryd  7380  smoel2  7445  omeu  7650  oeeui  7667  omabs  7712  omopth  7723  qliftel  7815  brecop  7825  eroveu  7827  erov  7829  ecopovtrn  7835  ixpsnf1o  7933  dom2lem  7980  xpsnen  8029  xpassen  8039  pw2f1olem  8049  xpf1o  8107  unxpdom  8152  domunfican  8218  preleq  8499  zfinf  8521  cantnfs  8548  tcvalg  8599  r0weon  8820  fseqenlem1  8832  acni2  8854  aceq1  8925  aceq0  8926  dfac2a  8937  dfac12lem2  8951  cardcf  9059  cfeq0  9063  cfsuc  9064  cff1  9065  cfss  9072  isf32lem5  9164  fin1a2lem6  9212  zfac  9267  brdom7disj  9338  brdom6disj  9339  axrepnd  9401  axunndlem1  9402  axinfnd  9413  axacndlem5  9418  axacnd  9419  zfcndrep  9421  zfcndinf  9425  zfcndac  9426  pwfseqlem4a  9468  pwfseqlem4  9469  gruina  9625  grothomex  9636  ordpipq  9749  elnpi  9795  genpass  9816  ltprord  9837  reclem2pr  9855  reclem3pr  9856  recexpr  9858  addsrmo  9879  mulsrmo  9880  addsrpr  9881  mulsrpr  9882  ltsosr  9900  mulgt0sr  9911  supsr  9918  ltresr  9946  axpre-lttrn  9972  axpre-mulgt0  9974  prime  11443  peano5uzti  11452  rexuz  11723  ltxr  11934  qbtwnre  12015  xmulneg1  12084  supxr2  12129  ixxval  12168  fzval  12313  preduz  12445  nn0opth2  13042  hashbclem  13219  hashf1lem2  13223  eqwrd  13329  swrdeq  13426  wrd2ind  13459  cshwcsh2id  13555  eqwrds3  13685  cleq1lem  13702  rtrclreclem3  13781  rtrclreclem4  13782  relexpindlem  13784  abslt  14035  absle  14036  lenegsq  14041  abs2difabs  14055  ello12  14228  elo12  14239  o1lo1  14249  rlimuni  14262  lo1resb  14276  o1resb  14278  2clim  14284  rlimcn2  14302  climcn2  14304  addcn2  14305  mulcn2  14307  o1of2  14324  sumeq1  14400  fsum2dlem  14482  modfsummod  14507  prodeq1f  14619  fprod2dlem  14691  znnenlem  14921  nndivdvds  14970  divalg2  15109  smupval  15191  gcdval  15199  gcdass  15245  lcmval  15286  lcmass  15308  rpexp  15413  pythagtriplem2  15503  pythagtrip  15520  vdwapun  15659  0ram  15705  ramub1lem2  15712  pwsle  16133  imasleval  16182  ismre  16231  ismri  16272  iscatd2  16323  dfiso2  16413  isssc  16461  funcpropd  16541  fullpropd  16561  fthres2b  16571  fthres2c  16572  setcsect  16720  prslem  16912  drsdir  16916  posi  16931  tosso  17017  ipoval  17135  ipolt  17140  odudlatb  17177  dirge  17218  gsumpropd2lem  17254  issgrpv  17267  issgrpn0  17268  mhmpropd  17322  mrcmndind  17347  mgmnsgrpex  17399  issubg3  17593  isga  17705  symgfixelq  17834  psgnfval  17901  psgnval  17908  isslw  18004  dprdw  18390  subgdmdprd  18414  drngpropd  18755  issubrg  18761  islmod  18848  lmodlema  18849  lmodprop2d  18906  lsslss  18942  lbspropd  19080  lbsacsbs  19137  aspval2  19328  psrbag  19345  pf1ind  19700  znleval  19884  islbs4  20152  islinds3  20154  mdetunilem4  20402  mdetunilem9  20407  istopg  20681  basis2  20736  tg2  20750  iscld  20812  neival  20887  isnei  20888  isneip  20890  neiptoptop  20916  neiptopnei  20917  neitr  20965  restlp  20968  iscn  21020  cnpval  21021  iscnp  21022  regsep  21119  1stcclb  21228  2ndc1stc  21235  2ndcctbss  21239  2ndcdisj  21240  llyi  21258  nllyi  21259  hausmapdom  21284  locfinnei  21307  comppfsc  21316  elkgen  21320  txbas  21351  txcls  21388  txcnpi  21392  ptpjopn  21396  txdis1cn  21419  txtube  21424  txcmplem1  21425  hausdiag  21429  tx1stc  21434  txkgen  21436  xkococnlem  21443  xkococn  21444  elqtop  21481  kqreglem1  21525  elmptrab  21611  isfbas  21614  elflim2  21749  elflim  21756  hauspwpwf1  21772  alexsublem  21829  ghmcnp  21899  qustgplem  21905  tsmssubm  21927  elutop  22018  ustuqtop4  22029  isucn  22063  iscfilu  22073  ispsmet  22090  ismet  22109  isxmet  22110  ismet2  22119  imasdsf1olem  22159  blres  22217  elmopn  22228  mopni  22278  neibl  22287  nrmmetd  22360  ngppropd  22422  elcncf  22673  mulc1cncf  22689  elpi1  22826  isclmp  22878  metcld2  23086  pmltpclem1  23198  ovolval  23223  itg1climres  23462  itg2val  23476  isibl  23513  itgeq1f  23519  itgresr  23526  iblcn  23546  itgfsum  23574  dvreslem  23654  dvfsumlem2  23771  deg1ldg  23833  vieta1  24048  ulm2  24120  sincosq2sgn  24232  sincosq4sgn  24234  efopn  24385  dvdsflsumcom  24895  fsumvma2  24920  logfac2  24923  dchrptlem1  24970  lgsdchrval  25060  2lgslem1a  25097  pntibndlem3  25262  pntlemi  25274  pntleme  25278  pnt3  25282  istrkgld  25339  istrkg2ld  25340  istrkg3ld  25341  axtgsegcon  25344  axtg5seg  25345  axtgpasch  25347  axtgupdim2  25351  legov  25461  islnopp  25612  ishpg  25632  iscgra1  25683  brcgr  25761  brbtwn2  25766  axsegconlem1  25778  axsegcon  25788  axcontlem10  25834  edgssv2  26071  uhgr2edg  26081  isfusgrf1  26193  edgnbusgreu  26250  cplgr3v  26312  vtxdun  26358  upgr2wlk  26545  upgrtrls  26579  upgristrl  26580  upgrf1istrl  26581  2pthnloop  26608  usgr2pth  26641  isclwlke  26654  isclwlkupgr  26655  iswwlksnx  26712  wlknewwlksn  26754  wwlksnfi  26782  wspthsnwspthsnon  26792  2pthon3v  26820  wwlks2onv  26828  elwwlks2on  26833  wpthswwlks2on  26835  rusgrnumwwlkl1  26844  rusgrnumwwlkb0  26847  clwwlksel  26894  clwwlksf  26895  erclwwlksnsym  26927  erclwwlksntr  26928  clwlksfoclwwlk  26943  0trl  26963  0spth  26967  0crct  26973  0cycl  26974  upgr4cycl4dv4e  27025  upgriseupth  27047  eupth2lem2  27059  3cyclfrgrrn1  27129  4cycl2vnunb  27134  frgrncvvdeqlem2  27144  frgr2wwlk1  27167  fusgr2wsp2nb  27172  extwwlkfablem2  27184  numclwwlkovfel2  27188  numclwwlk5  27216  vciOLD  27386  isvclem  27402  nmoofval  27587  isph  27647  norm3lemt  27979  isch2  28050  cmbr  28413  eigre  28664  eigorth  28667  nmopub  28737  nmfnleub  28754  cvbr  29111  mdbr  29123  dmdbr  29128  chrelat2  29199  mdsymlem2  29233  rexunirn  29303  ifeqeqx  29333  funcnvmptOLD  29441  funcnvmpt  29442  1stpreima  29458  fpwrelmapffslem  29481  isomnd  29675  archirng  29716  isslmd  29729  slmdlema  29730  orngmul  29777  dya2iocuni  30319  omsfval  30330  elcarsg  30341  itgeq12dv  30362  isrrvv  30479  reprinrn  30670  reprdifc  30679  istrkg2d  30718  axtgupdim2OLD  30720  brafs  30724  bnj956  30821  bnj1146  30836  bnj18eq1  30971  kur14  31172  pconncn  31180  cnpconn  31186  txpconn  31188  cvmscbv  31214  cvmcov  31219  cvmsi  31221  cvmsval  31222  cvmopnlem  31234  cvmlift2lem10  31268  cvmlift3lem2  31276  cvmlift3lem6  31280  cvmlift3lem7  31281  cvmlift3lem9  31283  cvmlift3  31284  mclsssvlem  31433  mclsind  31441  eldm3  31627  opelco3  31652  fv1stcnv  31654  fv2ndcnv  31655  dfon2lem6  31667  dfon2lem7  31668  dfon2lem8  31669  dfon2  31671  poseq  31724  soseq  31725  sltval  31774  nolt02o  31819  slelttr  31856  nocvxminlem  31867  elfuns  31997  brsuccf  32023  brofs  32087  5segofs  32088  brifs  32125  ifscgr  32126  brcolinear  32141  lineext  32158  brfs  32161  fscgr  32162  linecgr  32163  btwnconn1lem4  32172  btwnconn1lem8  32176  btwnconn1lem11  32179  btwnconn1lem12  32180  segcon2  32187  brsegle  32190  outsideofeq  32212  funray  32222  funline  32224  fvline  32226  linethru  32235  trer  32285  finminlem  32287  ivthALT  32305  filnetlem4  32351  knoppndvlem21  32498  bj-axrep1  32763  bj-axrep2  32764  bj-axrep3  32765  bj-axsep  32768  bj-ax8  32862  bj-rabeqd  32891  bj-axsep2  32896  csboprabg  33147  topdifinffinlem  33166  icoreval  33172  isbasisrelowllem1  33174  isbasisrelowllem2  33175  relowlssretop  33182  wl-ax11-lem8  33340  curf  33358  ptrest  33379  poimirlem1  33381  poimirlem13  33393  poimirlem14  33394  poimirlem22  33402  poimirlem24  33404  poimirlem26  33406  poimirlem27  33407  heicant  33415  mblfinlem3  33419  mblfinlem4  33420  mbfresfi  33427  itg2addnclem3  33434  itg2addnc  33435  itg2gt0cn  33436  areacirclem5  33475  cover2  33479  cover2g  33480  fdc  33512  fdc1  33513  heibor1  33580  bfp  33594  rngosn3  33694  drngoi  33721  isdrngo1  33726  isriscg  33754  isfldidl2  33839  islshpat  34123  lcvbr  34127  lshpsmreu  34215  ldual1dim  34272  cvrval  34375  cvrnbtwn3  34382  iscvlat2N  34430  ishlat3N  34460  hlrelat5N  34506  3dim0  34562  llnexatN  34626  islpln5  34640  islvol5  34684  pmapjat1  34958  ltrnu  35226  cdleme02N  35328  cdlemg33b  35814  cdlemg33c  35815  dvhb1dimN  36093  dibelval3  36255  dibopelval3  36256  dib1dim  36273  dibglbN  36274  diblsmopel  36279  dicval  36284  dicopelval  36285  dicelval3  36288  dicelval1sta  36295  dihopelvalcpre  36356  dih1dimatlem  36437  dihpN  36444  dihjatcclem4  36529  lpolsetN  36590  mapdpglem3  36783  hdmapglem7a  37038  mrefg2  37089  mzpclval  37107  eldiophb  37139  eldioph2lem1  37142  eldioph3  37148  lzenom  37152  diophin  37155  eldiophss  37157  diophrex  37158  eq0rabdioph  37159  pellexlem3  37214  elpell1qr  37230  elpell14qr  37232  elpell1234qr  37234  jm2.27  37394  rmydioph  37400  expdiophlem1  37407  expdioph  37409  pw2f1ocnv  37423  hbtlem1  37512  hbtlem7  37514  dgraalem  37534  dgraaub  37537  ifpbi2  37630  inintabd  37704  cnvcnvintabd  37725  cnvintabd  37728  clcnvlem  37749  iunrelexpmin1  37819  uneqsn  38141  k0004lem2  38266  binomcxplemnotnn0  38375  2sbc6g  38436  2sbc5g  38437  iotasbc  38440  dropab1  38471  dropab2  38472  cbvmpt21  39098  disjinfi  39196  mapsnend  39207  dmrelrnrel  39235  mullimc  39648  mullimcf  39655  limsuppnfd  39734  limsuppnf  39743  limsupre2  39757  limsupre2mpt  39762  limsupre3  39765  limsupre3mpt  39766  limsupre3uzlem  39767  fourierdlem42  40129  fourierdlem48  40134  fourierdlem50  40136  fourierdlem51  40137  fourierdlem54  40140  fourierdlem86  40172  ovnval2  40522  ovnsubaddlem1  40547  hoiqssbl  40602  vonicclem2  40661  dfdfat2  40974  2ffzoeq  41101  pfxeq  41169  mgmhmpropd  41550  ismhm0  41570  isrnghm  41657  rngcsect  41745  rngcinv  41746  rngcsectALTV  41757  rngcinvALTV  41758  ringcsect  41796  ringcinv  41797  ringcsectALTV  41820  ringcinvALTV  41821  lmod1  42046  elbigo2  42111
  Copyright terms: Public domain W3C validator