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

Theorem anbi1d 709
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  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
anbi1d  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )

Proof of Theorem anbi1d
StepHypRef Expression
1 bid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21a1d 26 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32rd 644 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  anbi1  711  anbi12d  715  bi2anan9  881  pm5.71  944  cador  1504  drsb1  2177  eleq1d  2485  rexeqf  2956  reueq1f  2957  rmoeq1f  2958  rabeqf  3009  vtocl2gaf  3084  vtocl4ga  3089  alexeqg  3138  elrabi  3163  reu2eqd  3205  sbc2or  3246  sbc5  3262  rexss  3466  psstr  3507  ineq1  3595  difin2  3673  r19.28z  3829  r19.28zv  3832  rabsnifsb  4006  ssunsn2  4097  preq12bg  4117  prel12g  4118  opeq1  4125  eluni  4160  csbuni  4185  disjxun  4359  mpteq12f  4438  axrep1  4475  axrep2  4476  axrep3  4477  zfrepclf  4480  axsep  4483  axsep2  4485  zfauscl  4486  reusv2lem4  4566  rabxfrd  4580  opthg  4634  otthg  4642  copsexg  4644  euotd  4659  elopab  4666  pocl  4719  xpeq1  4805  elxpi  4807  vtoclr  4836  opbrop  4871  opelresg  5069  resopab2  5110  dflim2  5436  fun11  5604  feq2  5667  f1eq2  5730  f1eq3  5731  foeq2  5745  brprcneu  5813  ssimaexg  5886  dmfco  5894  fndmdif  5940  respreima  5963  isoeq5  6168  isoini  6183  isopolem  6190  f1oiso  6196  f1oiso2  6197  riotaeqdv  6207  oprabid  6271  oprabv  6292  mpt2eq123  6303  mpt2eq123dva  6305  eloprabga  6336  resoprab  6345  resoprab2  6346  elrnmpt2res  6363  ov  6369  ov3  6386  ov6g  6387  ovg  6388  caoftrn  6519  uniuni  6553  limuni3  6632  elxp4  6690  elxp5  6691  opabex3d  6724  opabex3  6725  opiota  6805  eloprabi  6808  cnvf1o  6845  frxp  6856  xporderlem  6857  poxp  6858  fnwelem  6861  suppimacnv  6875  rexsupp  6883  mpt2curryd  6966  smoel2  7032  omeu  7236  oeeui  7253  omabs  7298  omopth  7309  qliftel  7396  brecop  7406  eroveu  7408  erov  7410  ecopovtrn  7416  ixpsnf1o  7512  dom2lem  7558  xpsnen  7604  xpassen  7614  pw2f1olem  7624  xpf1o  7682  unxpdom  7727  domunfican  7792  preleq  8070  zfinf  8092  cantnfs  8118  tcvalg  8169  r0weon  8390  fseqenlem1  8401  acni2  8423  aceq1  8494  aceq0  8495  dfac2a  8506  dfac12lem2  8520  cardcf  8628  cfeq0  8632  cfsuc  8633  cff1  8634  cfss  8641  isf32lem5  8733  fin1a2lem6  8781  zfac  8836  brdom7disj  8905  brdom6disj  8906  axrepnd  8965  axunndlem1  8966  axinfnd  8977  axacndlem5  8982  axacnd  8983  zfcndrep  8985  zfcndinf  8989  zfcndac  8990  pwfseqlem4a  9032  pwfseqlem4  9033  gruina  9189  grothomex  9200  ordpipq  9313  elnpi  9359  genpass  9380  ltprord  9401  reclem2pr  9419  reclem3pr  9420  recexpr  9422  addsrmo  9443  mulsrmo  9444  addsrpr  9445  mulsrpr  9446  ltsosr  9464  mulgt0sr  9475  supsr  9482  ltresr  9510  axpre-lttrn  9536  axpre-mulgt0  9538  prime  10962  peano5uzti  10971  rexuz  11155  ltxr  11361  qbtwnre  11438  xmulneg1  11501  supxr2  11545  ixxval  11589  fzval  11732  preduz  11857  nn0opth2  12403  hashbclem  12558  hashf1lem2  12562  eqwrd  12651  swrdeq  12741  wrd2ind  12775  cshwcsh2id  12868  cleq1lem  12985  rtrclreclem3  13062  rtrclreclem4  13063  relexpindlem  13065  abslt  13316  absle  13317  lenegsq  13322  abs2difabs  13336  ello12  13518  elo12  13529  o1lo1  13539  rlimuni  13552  lo1resb  13566  o1resb  13568  2clim  13574  rlimcn2  13592  climcn2  13594  addcn2  13595  mulcn2  13597  o1of2  13614  sumeq1  13693  fsum2dlem  13769  modfsummod  13792  prodeq1f  13900  fprod2dlem  13972  znnenlem  14202  nndivdvds  14249  divalg2  14324  smupval  14400  gcdval  14408  gcdass  14451  lcmval  14493  lcmvalOLD  14494  lcmass  14517  rpexp  14610  pythagtriplem2  14705  pythagtrip  14722  vdwapun  14862  0ram  14916  ramub1lem2  14923  pwsle  15328  imasleval  15385  ismre  15434  ismri  15475  iscatd2  15525  dfiso2  15615  isssc  15663  funcpropd  15743  fullpropd  15763  fthres2b  15773  fthres2c  15774  setcsect  15922  prslem  16114  drsdir  16118  posi  16133  tosso  16220  ipoval  16338  ipolt  16343  odudlatb  16380  dirge  16421  gsumpropd2lem  16454  issgrpv  16467  issgrpn0  16468  mhmpropd  16526  mrcmndind  16551  mgmnsgrpex  16603  issubg3  16773  isga  16883  symgfixelq  17012  psgnfval  17079  psgnval  17086  isslw  17198  dprdw  17580  subgdmdprd  17605  drngpropd  17940  issubrg  17946  islmod  18033  lmodlema  18034  lmodprop2d  18088  lsslss  18122  lbspropd  18260  lbsacsbs  18317  aspval2  18509  psrbag  18526  pf1ind  18881  znleval  19062  islbs4  19327  islinds3  19329  mdetunilem4  19577  mdetunilem9  19582  istopg  19862  basis2  19903  tg2  19917  iscld  19979  neival  20055  isnei  20056  isneip  20058  neiptoptop  20084  neiptopnei  20085  neitr  20133  restlp  20136  iscn  20188  cnpval  20189  iscnp  20190  regsep  20287  nrmsep3  20308  1stcclb  20396  2ndc1stc  20403  2ndcctbss  20407  2ndcdisj  20408  llyi  20426  nllyi  20427  hausmapdom  20452  locfinnei  20475  comppfsc  20484  elkgen  20488  txbas  20519  txcls  20556  txcnpi  20560  ptpjopn  20564  txdis1cn  20587  txtube  20592  txcmplem1  20593  hausdiag  20597  tx1stc  20602  txkgen  20604  xkococnlem  20611  xkococn  20612  elqtop  20649  kqreglem1  20693  elmptrab  20779  isfbas  20781  elflim2  20916  elflim  20923  hauspwpwf1  20939  alexsublem  20996  ghmcnp  21066  qustgplem  21072  tsmssubm  21094  elutop  21185  ustuqtop4  21196  isucn  21230  iscfilu  21240  ispsmet  21257  ismet  21275  isxmet  21276  ismet2  21285  imasdsf1olem  21325  blres  21383  elmopn  21394  mopni  21444  neibl  21453  nrmmetd  21526  ngppropd  21582  elcncf  21858  mulc1cncf  21874  elpi1  22013  metcld2  22213  pmltpclem1  22336  ovolval  22363  ovolvalOLD  22364  itg1climres  22609  itg2val  22623  isibl  22660  itgeq1f  22666  itgresr  22673  iblcn  22693  itgfsum  22721  dvreslem  22801  dvfsumlem2  22916  deg1ldg  22978  vieta1  23202  ulm2  23277  sincosq2sgn  23391  sincosq4sgn  23393  efopn  23540  dvdsflsumcom  24054  fsumvma2  24079  logfac2  24082  dchrptlem1  24129  lgsdchrval  24212  pntibndlem3  24367  pntlemi  24379  pntleme  24383  pnt3  24387  istrkgld  24444  istrkg2ld  24445  istrkg3ld  24446  axtgsegcon  24449  axtg5seg  24450  axtgpasch  24452  axtgupdim2  24456  legov  24567  islnopp  24718  ishpg  24738  iscgra1  24789  brcgr  24867  brbtwn2  24872  axsegconlem1  24884  axsegcon  24894  axcontlem10  24940  usgra2edg  25046  trls  25203  istrl2  25205  trlon  25207  is2wlk  25232  spths  25234  0spth  25238  pthon  25242  spthon  25249  isspthonpth  25251  usgra2wlkspthlem1  25284  0crct  25291  0cycl  25292  usgrcyclnl2  25306  wwlknprop  25351  vfwlkniswwlkn  25371  wwlknext  25389  wwlknfi  25403  clwlk  25418  isclwlk  25421  clwlkcompim  25429  clwwlkn2  25440  clwwlknimp  25441  clwwlkel  25458  clwwlkf  25459  clwwlkext2edg  25467  wwlkext2clwwlk  25468  wwlksubclwwlk  25469  erclwwlknsym  25491  erclwwlkntr  25492  clwlkfoclwwlk  25510  el2wlkonotot0  25537  2spontn0vne  25552  rusgranumwlkl1  25612  rusgranumwlklem3  25616  rusgranumwlkb0  25618  rusgra0edg  25620  eupath2lem2  25643  3cyclfrgrarn1  25677  4cycl2vnunb  25682  frg2wot1  25722  usg2spot2nb  25730  extwwlkfablem2  25743  numclwwlkovfel2  25748  numclwwlkovf2  25749  numclwwlkovf2ex  25751  numclwwlkovgel  25753  numclwwlkovgelim  25754  numclwlk2lem2f  25768  numclwlk2lem2f1o  25770  numclwwlk5  25777  drngoi  26072  rngosn3  26091  vci  26104  isvclem  26133  nmoofval  26340  isph  26400  norm3lemt  26742  isch2  26813  cmbr  27174  eigre  27425  eigorth  27428  nmopub  27498  nmfnleub  27515  cvbr  27872  mdbr  27884  dmdbr  27889  chrelat2  27960  mdsymlem2  27994  rexunirn  28064  ifeqeqx  28099  funcnvmptOLD  28211  funcnvmpt  28212  1stpreima  28228  fpwrelmapffslem  28262  isomnd  28410  archirng  28451  isslmd  28464  slmdlema  28465  orngmul  28513  dya2iocuni  29052  omsfval  29065  omsfvalOLD  29069  elcarsg  29084  itgeq12dv  29106  isrrvv  29223  istrkg2d  29430  axtgupdim2OLD  29432  brafs  29436  bnj956  29535  bnj1146  29550  bnj18eq1  29685  kur14  29886  pconcn  29894  cnpcon  29900  txpcon  29902  cvmscbv  29928  cvmcov  29933  cvmsi  29935  cvmsval  29936  cvmopnlem  29948  cvmlift2lem10  29982  cvmlift3lem2  29990  cvmlift3lem6  29994  cvmlift3lem7  29995  cvmlift3lem9  29997  cvmlift3  29998  mclsssvlem  30147  mclsind  30155  eldm3  30348  opelco3  30366  fv1stcnv  30368  fv2ndcnv  30369  dfon2lem6  30380  dfon2lem7  30381  dfon2lem8  30382  dfon2  30384  poseq  30437  soseq  30438  sltval  30480  nodenselem5  30518  nocvxminlem  30523  elfuns  30626  brsuccf  30652  brofs  30716  5segofs  30717  brifs  30754  ifscgr  30755  brcolinear  30770  lineext  30787  brfs  30790  fscgr  30791  linecgr  30792  btwnconn1lem4  30801  btwnconn1lem8  30805  btwnconn1lem11  30808  btwnconn1lem12  30809  segcon2  30816  brsegle  30819  outsideofeq  30841  funray  30851  funline  30853  fvline  30855  linethru  30864  trer  30916  finminlem  30918  ivthALT  30935  filnetlem4  30981  bj-axrep1  31314  bj-axrep2  31315  bj-axrep3  31316  bj-axsep  31319  bj-eleq1w  31366  bj-ax8  31406  bj-rabeqd  31434  bj-axsep2  31439  csboprabg  31638  topdifinffinlem  31657  icoreval  31663  isbasisrelowllem1  31665  isbasisrelowllem2  31666  relowlssretop  31673  wl-ax11-lem8  31829  ptrest  31846  poimirlem1  31848  poimirlem13  31860  poimirlem14  31861  poimirlem22  31869  poimirlem24  31871  poimirlem26  31873  poimirlem27  31874  heicant  31882  mblfinlem3  31886  mblfinlem4  31887  mbfresfi  31894  itg2addnclem3  31902  itg2addnc  31903  itg2gt0cn  31904  areacirclem5  31943  cover2  31947  cover2g  31948  fdc  31981  fdc1  31982  heibor1  32049  bfp  32063  isdrngo1  32102  isriscg  32130  isfldidl2  32209  islshpat  32495  lcvbr  32499  lshpsmreu  32587  ldual1dim  32644  cvrval  32747  cvrnbtwn3  32754  iscvlat2N  32802  ishlat3N  32832  hlrelat5N  32878  3dim0  32934  llnexatN  32998  islpln5  33012  islvol5  33056  pmapjat1  33330  ltrnu  33598  cdleme02N  33700  cdlemg33b  34186  cdlemg33c  34187  dvhb1dimN  34465  dibelval3  34627  dibopelval3  34628  dib1dim  34645  dibglbN  34646  diblsmopel  34651  dicval  34656  dicopelval  34657  dicelval3  34660  dicelval1sta  34667  dihopelvalcpre  34728  dih1dimatlem  34809  dihpN  34816  dihjatcclem4  34901  lpolsetN  34962  mapdpglem3  35155  hdmapglem7a  35410  mrefg2  35461  mzpclval  35479  eldiophb  35511  eldioph2lem1  35514  eldioph3  35520  lzenom  35524  diophin  35527  eldiophss  35529  diophrex  35530  eq0rabdioph  35531  pellexlem3  35588  elpell1qr  35606  elpell14qr  35608  elpell1234qr  35610  jm2.27  35776  rmydioph  35782  expdiophlem1  35789  expdioph  35791  pw2f1ocnv  35805  hbtlem1  35895  hbtlem7  35897  dgraalem  35920  dgraalemOLD  35921  dgraaub  35926  dgraaubOLD  35927  ifpbi2  36023  inintabd  36098  cnvcnvintabd  36119  cnvintabd  36122  clcnvlem  36143  iunrelexpmin1  36213  binomcxplemnotnn0  36618  2sbc6g  36679  2sbc5g  36680  iotasbc  36683  dropab1  36713  dropab2  36714  disjinfi  37372  mullimc  37579  mullimcf  37586  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem48  37901  fourierdlem50  37903  fourierdlem51  37904  fourierdlem54  37907  fourierdlem86  37939  ovnval2  38214  ovnsubaddlem1  38239  dfdfat2  38446  pfxeq  38758  2ffzoeq  38861  edgassv2  39033  usgr2edg  39040  isfusgrf1  39123  edgnbusgreu  39177  cplgr3v  39230  spthdifv  39257  usgra2pth  39259  edgssv2ALT  39304  edgssv2  39305  isfusgra0  39328  fusgraimpclALT2  39334  mgmhmpropd  39376  ismhm0  39396  isrnghm  39483  rngcsect  39573  rngcinv  39574  rngcsectALTV  39585  rngcinvALTV  39586  ringcsect  39624  ringcinv  39625  ringcsectALTV  39648  ringcinvALTV  39649  lmod1  39878  elbigo2  39956
  Copyright terms: Public domain W3C validator