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

Theorem anbi1d 697
Description: Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-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 25 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32rd 633 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  anbi1  699  anbi12d  703  bi2anan9  861  pm5.71  920  cador  1435  drsb1  2065  eleq1  2493  rexeqf  2904  reueq1f  2905  rmoeq1f  2906  rabeqf  2955  vtocl2gaf  3026  vtocl4ga  3031  alexeqg  3077  alexeq  3078  elrabi  3103  sbc2or  3183  sbc5  3199  rexss  3407  psstr  3448  ineq1  3533  difin2  3600  r19.28z  3760  r19.28zv  3763  rabsnifsb  3931  ssunsn2  4020  preq12bg  4039  prel12g  4040  opeq1  4047  eluni  4082  csbuni  4107  disjxun  4278  mpteq12f  4356  axrep1  4392  axrep2  4393  axrep3  4394  zfrepclf  4397  axsep  4400  axsep2  4402  zfauscl  4403  reusv2lem4  4484  rabxfrd  4501  opthg  4555  copsexg  4564  copsexgOLD  4565  euotd  4580  elopab  4585  pocl  4635  dflim2  4762  xpeq1  4841  elxpi  4843  vtoclr  4870  opbrop  4903  opelresg  5105  resopab2  5143  fun11  5471  feq2  5531  f1eq2  5590  f1eq3  5591  foeq2  5605  brprcneu  5672  ssimaexg  5745  dmfco  5753  fndmdif  5795  rexsuppOLD  5816  respreima  5820  isoeq5  6001  isoini  6016  isopolem  6023  f1oiso  6029  f1oiso2  6030  riotaeqdv  6040  oprabid  6104  mpt2eq123  6134  mpt2eq123dva  6136  eloprabga  6166  resoprab  6175  resoprab2  6176  elrnmpt2res  6193  ov  6199  ov3  6216  ov6g  6217  ovg  6218  caoftrn  6344  uniuni  6374  limuni3  6452  elxp4  6511  elxp5  6512  opabex3d  6544  opabex3  6545  opiota  6622  eloprabi  6625  cnvf1o  6660  frxp  6671  xporderlem  6672  poxp  6673  fnwelem  6676  suppimacnv  6690  rexsupp  6696  smoel2  6810  omeu  7012  oeeui  7029  omabs  7074  omopth  7085  qliftel  7171  brecop  7181  eroveu  7183  erov  7185  ecopovtrn  7191  th3qlem2  7195  th3q  7197  ixpsnf1o  7291  dom2lem  7337  xpsnen  7383  xpassen  7393  pw2f1olem  7403  xpf1o  7461  unxpdom  7508  domunfican  7572  preleq  7811  zfinf  7833  cantnfs  7862  cantnfsOLD  7892  tcvalg  7946  r0weon  8167  fseqenlem1  8182  acni2  8204  aceq1  8275  aceq0  8276  dfac2a  8287  dfac12lem2  8301  cardcf  8409  cfeq0  8413  cfsuc  8414  cff1  8415  cfss  8422  isf32lem5  8514  fin1a2lem6  8562  zfac  8617  brdom7disj  8686  brdom6disj  8687  axrepnd  8746  axunndlem1  8747  axinfnd  8761  axacndlem5  8766  axacnd  8767  zfcndrep  8769  zfcndinf  8773  zfcndac  8774  pwfseqlem4a  8816  pwfseqlem4  8817  gruina  8973  grothomex  8984  ordpipq  9099  elnpi  9145  genpass  9166  ltprord  9187  reclem2pr  9205  reclem3pr  9206  recexpr  9208  ltsosr  9249  mulgt0sr  9260  supsr  9267  ltresr  9295  axpre-lttrn  9321  axpre-mulgt0  9323  prime  10710  peano5uzti  10719  uzindOLD  10724  rexuz  10893  ltxr  11083  qbtwnre  11157  xmulneg1  11220  supxr2  11264  ixxval  11296  fzval  11426  nn0opth2  12034  hashbclem  12189  hashf1lem2  12193  eqwrd  12249  swrdeq  12324  wrd2ind  12356  abslt  12786  absle  12787  lenegsq  12792  abs2difabs  12806  ello12  12978  elo12  12989  o1lo1  12999  rlimuni  13012  lo1resb  13026  o1resb  13028  2clim  13034  rlimcn2  13052  climcn2  13054  addcn2  13055  mulcn2  13057  o1of2  13074  sumeq1  13150  fsum2dlem  13221  znnenlem  13477  nndivdvds  13524  divalg2  13592  smupval  13667  gcdval  13675  gcdass  13712  rpexp  13789  pythagtriplem2  13867  pythagtrip  13884  vdwapun  14018  0ram  14064  ramub1lem2  14071  pwsle  14413  imasleval  14462  ismre  14511  ismri  14552  iscatd2  14602  isssc  14716  funcpropd  14793  fullpropd  14813  fthres2b  14823  fthres2c  14824  setcsect  14940  prslem  15084  drsdir  15088  posi  15103  tosso  15189  ipoval  15307  ipolt  15312  odudlatb  15349  dirge  15390  mndpropd  15429  mhmpropd  15453  mrcmndind  15476  issubg3  15679  isga  15789  symgfixelq  15918  psgnfval  15986  psgnval  15993  isslw  16087  dprdw  16468  dprdwOLD  16474  subgdmdprd  16505  drngpropd  16783  issubrg  16789  islmod  16876  lmodlema  16877  lmodprop2d  16931  lsslss  16964  lbspropd  17102  lbsacsbs  17159  aspval2  17339  psrbag  17365  znleval  17829  islbs4  18103  islinds3  18105  mdetunilem4  18263  mdetunilem9  18268  istopg  18350  basis2  18398  tg2  18412  iscld  18473  neival  18548  isnei  18549  isneip  18551  neiptoptop  18577  neiptopnei  18578  neitr  18626  restlp  18629  iscn  18681  cnpval  18682  iscnp  18683  regsep  18780  nrmsep3  18801  1stcclb  18890  2ndc1stc  18897  2ndcctbss  18901  2ndcdisj  18902  llyi  18920  nllyi  18921  hausmapdom  18946  elkgen  18951  txbas  18982  txcls  19019  txcnpi  19023  ptpjopn  19027  txdis1cn  19050  txtube  19055  txcmplem1  19056  hausdiag  19060  tx1stc  19065  txkgen  19067  xkococnlem  19074  xkococn  19075  elqtop  19112  kqreglem1  19156  elmptrab  19242  isfbas  19244  elflim2  19379  elflim  19386  hauspwpwf1  19402  alexsublem  19458  ghmcnp  19527  divstgplem  19533  tsmssubm  19558  elutop  19650  ustuqtop4  19661  isucn  19695  iscfilu  19705  ispsmet  19722  ismet  19740  isxmet  19741  ismet2  19750  imasdsf1olem  19790  blres  19848  elmopn  19859  mopni  19909  neibl  19918  nrmmetd  20009  ngppropd  20065  elcncf  20307  mulc1cncf  20323  elpi1  20459  metcld2  20659  pmltpclem1  20774  ovolval  20799  itg1climres  21034  itg2val  21048  isibl  21085  itgeq1f  21091  itgresr  21098  iblcn  21118  itgfsum  21146  dvreslem  21226  dvfsumlem2  21341  pf1ind  21406  deg1ldg  21448  vieta1  21663  ulm2  21735  sincosq2sgn  21846  sincosq4sgn  21848  efopn  21988  dvdsflsumcom  22413  fsumvma2  22438  logfac2  22441  dchrptlem1  22488  lgsdchrval  22571  pntibndlem3  22726  pntlemi  22738  pntleme  22742  pnt3  22746  istrkg2d  22807  axtgsegcon  22810  axtg5seg  22811  axtgpasch  22813  axtgupdim2  22817  legov  22892  brcgr  22969  brbtwn2  22974  axsegconlem1  22986  axsegcon  22996  axcontlem10  23042  usgra2edg  23124  trls  23258  istrl2  23260  trlon  23262  is2wlk  23287  spths  23289  0spth  23293  pthon  23297  spthon  23304  isspthonpth  23306  0crct  23335  0cycl  23336  usgrcyclnl2  23350  eupath2lem2  23422  drngoi  23717  rngosn3  23736  vci  23749  isvclem  23778  nmoofval  23985  isph  24045  norm3lemt  24377  isch2  24449  cmbr  24810  eigre  25062  eigorth  25065  nmopub  25135  nmfnleub  25152  cvbr  25509  mdbr  25521  dmdbr  25526  chrelat2  25597  mdsymlem2  25631  rexunirn  25699  ifeqeqx  25726  funcnvmptOLD  25810  funcnvmpt  25811  1stpreima  25825  fpwrelmapffslem  25857  isomnd  25988  archirng  26029  isslmd  26067  slmdlema  26068  gsumpropd2lem  26093  dya2iocuni  26552  itgeq12dv  26560  isrrvv  26674  brafs  26844  kur14  26952  pconcn  26961  cnpcon  26967  txpcon  26969  cvmscbv  26995  cvmcov  27000  cvmsi  27002  cvmsval  27003  cvmopnlem  27015  cvmlift2lem10  27049  cvmlift3lem2  27057  cvmlift3lem6  27061  cvmlift3lem7  27062  cvmlift3lem9  27064  cvmlift3  27065  relexp0  27178  relexpsucr  27179  relexpsucl  27181  relexpcnv  27182  relexpdm  27184  relexprn  27185  relexpadd  27187  relexpindlem  27188  rtrclreclem.trans  27195  rtrclreclem.min  27196  prodeq1f  27268  fprod2dlem  27338  eldm3  27419  opelco3  27436  dfon2lem6  27448  dfon2lem7  27449  dfon2lem8  27450  dfon2  27452  preduz  27508  poseq  27561  soseq  27562  sltval  27635  nodenselem5  27673  nocvxminlem  27678  elfuns  27793  brofs  27883  5segofs  27884  brifs  27921  ifscgr  27922  brcolinear  27937  lineext  27954  brfs  27957  fscgr  27958  linecgr  27959  btwnconn1lem4  27968  btwnconn1lem8  27972  btwnconn1lem11  27975  btwnconn1lem12  27976  segcon2  27983  brsegle  27986  outsideofeq  28008  funray  28018  funline  28020  fvline  28022  linethru  28031  wl-ax11-lem8  28252  ptrest  28269  heicant  28270  mblfinlem3  28274  mblfinlem4  28275  mbfresfi  28282  itg2addnclem3  28289  itg2addnc  28290  itg2gt0cn  28291  areacirclem5  28332  trer  28355  finminlem  28357  ivthALT  28374  locfinnei  28418  comppfsc  28423  filnetlem4  28446  cover2  28451  cover2g  28452  fdc  28485  fdc1  28486  heibor1  28553  bfp  28567  isdrngo1  28606  isriscg  28634  isfldidl2  28713  mrefg2  28888  mzpclval  28906  eldiophb  28940  eldioph2lem1  28943  eldioph3  28949  lzenom  28953  diophin  28956  eldiophss  28958  diophrex  28959  eq0rabdioph  28960  pellexlem3  29017  elpell1qr  29033  elpell14qr  29035  elpell1234qr  29037  jm2.27  29202  rmydioph  29208  expdiophlem1  29215  expdioph  29217  pw2f1ocnv  29231  hbtlem1  29324  hbtlem7  29326  dgraalem  29347  dgraaub  29350  2sbc6g  29514  2sbc5g  29515  iotasbc  29518  dropab1  29548  dropab2  29549  dfdfat2  29883  otthg  29976  oprabv  30003  2ffzoeq  30060  modfsummod  30091  usgra2wlkspthlem1  30142  spthdifv  30145  usgra2pth  30147  wwlknprop  30166  vfwlkniswwlkn  30186  wwlknext  30202  wwlknfi  30216  el2wlkonotot0  30237  2spontn0vne  30252  clwlk  30264  isclwlk  30267  clwlkcompim  30273  clwwlkn2  30284  clwwlknimp  30285  clwwlkel  30301  clwwlkf  30302  clwwlkext2edg  30310  wwlkext2clwwlk  30311  wwlksubclwwlk  30312  erclwwlktr0  30325  erclwwlknsym  30346  erclwwlkntr  30347  clwlkfoclwwlk  30364  rusgranumwlkl1  30405  rusgranumwlklem3  30415  rusgranumwlkb0  30417  rusgra0edg  30419  3cyclfrgrarn1  30450  4cycl2vnunb  30455  frg2wot1  30496  usg2spot2nb  30504  extwwlkfablem2  30517  numclwwlkovfel2  30522  numclwwlkovf2  30523  numclwwlkovf2ex  30525  numclwwlkovgel  30527  numclwwlkovgelim  30528  numclwlk2lem2f  30542  numclwlk2lem2f1o  30544  numclwwlk5  30551  lmod1  30743  bnj956  31472  bnj1146  31487  bnj18eq1  31622  bj-axrep1  31929  bj-axrep2  31930  bj-axrep3  31931  bj-axsep  31934  bj-eleq1w  31970  bj-rabeqd  32010  islshpat  32235  lcvbr  32239  lshpsmreu  32327  ldual1dim  32384  cvrval  32487  cvrnbtwn3  32494  iscvlat2N  32542  ishlat3N  32572  hlrelat5N  32618  3dim0  32674  llnexatN  32738  islpln5  32752  islvol5  32796  pmapjat1  33070  ltrnu  33338  cdleme02N  33439  cdlemg33b  33924  cdlemg33c  33925  dvhb1dimN  34203  dibelval3  34365  dibopelval3  34366  dib1dim  34383  dibglbN  34384  diblsmopel  34389  dicval  34394  dicopelval  34395  dicelval3  34398  dicelval1sta  34405  dihopelvalcpre  34466  dih1dimatlem  34547  dihpN  34554  dihjatcclem4  34639  lpolsetN  34700  mapdpglem3  34893  hdmapglem7a  35148
  Copyright terms: Public domain W3C validator