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

Theorem anbi1d 687
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 24 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32rd 623 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  anbi1  689  anbi12d  693  bi2anan9  845  pm5.71  904  cador  1401  drsb1  2113  eleq1  2497  rexeqf  2902  reueq1f  2903  rmoeq1f  2904  rabeqf  2950  vtocl2gaf  3019  alexeq  3066  ceqex  3067  elrabi  3091  sbc2or  3170  sbc5  3186  rexss  3411  psstr  3452  ineq1  3536  difin2  3604  r19.28z  3721  r19.28zv  3724  ssunsn2  3959  preq12bg  3978  opeq1  3985  eluni  4019  disjxun  4211  mpteq12f  4286  axrep1  4322  axrep2  4323  axrep3  4324  zfrepclf  4327  axsep  4330  axsep2  4332  zfauscl  4333  opthg  4437  copsexg  4443  euotd  4458  elopab  4463  pocl  4511  dflim2  4638  uniuni  4717  reusv2lem4  4728  rabxfrd  4745  limuni3  4833  xpeq1  4893  elxpi  4895  vtoclr  4923  opbrop  4956  opelresg  5154  resopab2  5191  elxp4  5358  elxp5  5359  fun11  5517  feq2  5578  f1eq2  5636  f1eq3  5637  foeq2  5651  brprcneu  5722  ssimaexg  5790  dmfco  5798  fndmdif  5835  rexsupp  5856  respreima  5860  opabex3d  5990  opabex3  5991  isoeq5  6044  isoini  6059  isopolem  6066  f1oiso  6072  f1oiso2  6073  oprabid  6106  mpt2eq123  6134  mpt2eq123dva  6136  eloprabga  6161  resoprab  6167  resoprab2  6168  ov  6194  ov3  6211  ov6g  6212  ovg  6213  caoftrn  6340  eloprabi  6414  cnvf1o  6446  frxp  6457  xporderlem  6458  poxp  6459  fnwelem  6462  opiota  6536  riotaeqdv  6551  smoel2  6626  omeu  6829  oeeui  6846  omabs  6891  omopth  6902  qliftel  6988  brecop  6998  eroveu  7000  erov  7002  ecopovtrn  7008  th3qlem2  7012  th3q  7014  ixpsnf1o  7103  dom2lem  7148  xpsnen  7193  xpassen  7203  pw2f1olem  7213  xpf1o  7270  unxpdom  7317  domunfican  7380  preleq  7573  zfinf  7595  cantnfs  7622  tcvalg  7678  r0weon  7895  fseqenlem1  7906  acni2  7928  aceq1  7999  aceq0  8000  dfac2a  8011  dfac12lem2  8025  cardcf  8133  cfeq0  8137  cfsuc  8138  cff1  8139  cfss  8146  isf32lem5  8238  fin1a2lem6  8286  zfac  8341  brdom7disj  8410  brdom6disj  8411  axrepnd  8470  axunndlem1  8471  axinfnd  8482  axacndlem5  8487  axacnd  8488  zfcndrep  8490  zfcndinf  8494  zfcndac  8495  pwfseqlem4a  8537  pwfseqlem4  8538  gruina  8694  grothomex  8705  ordpipq  8820  elnpi  8866  genpass  8887  ltprord  8908  reclem2pr  8926  reclem3pr  8927  recexpr  8929  ltsosr  8970  mulgt0sr  8981  supsr  8988  ltresr  9016  axpre-lttrn  9042  axpre-mulgt0  9044  prime  10351  peano5uzti  10360  uzindOLD  10365  rexuz  10528  ltxr  10716  qbtwnre  10786  xmulneg1  10849  supxr2  10893  ixxval  10925  fzval  11046  nn0opth2  11566  hashbclem  11702  hashf1lem2  11706  abslt  12119  absle  12120  lenegsq  12125  abs2difabs  12139  ello12  12311  elo12  12322  o1lo1  12332  rlimuni  12345  lo1resb  12359  o1resb  12361  2clim  12367  rlimcn2  12385  climcn2  12387  addcn2  12388  mulcn2  12390  o1of2  12407  sumeq1f  12483  fsum2dlem  12555  znnenlem  12812  nndivdvds  12859  divalg2  12926  smupval  13001  gcdval  13009  gcdass  13046  rpexp  13121  pythagtriplem2  13192  pythagtrip  13209  vdwapun  13343  0ram  13389  ramub1lem2  13396  pwsle  13715  imasleval  13767  ismre  13816  ismri  13857  iscatd2  13907  isssc  14021  funcpropd  14098  fullpropd  14118  fthres2b  14128  fthres2c  14129  setcsect  14245  prslem  14389  drsdir  14393  posi  14408  tosso  14466  ipoval  14581  ipolt  14586  odudlatb  14623  dirge  14683  mndpropd  14722  mhmpropd  14745  issubg3  14961  isga  15069  isslw  15243  dprdw  15569  subgdmdprd  15593  drngpropd  15863  issubrg  15869  islmod  15955  lmodlema  15956  lmodprop2d  16007  lsslss  16038  lbspropd  16172  lbsacsbs  16229  aspval2  16406  psrbag  16432  znleval  16836  istopg  16969  basis2  17017  tg2  17031  iscld  17092  neival  17167  isnei  17168  isneip  17170  neiptoptop  17196  neiptopnei  17197  neitr  17245  restlp  17248  iscn  17300  cnpval  17301  iscnp  17302  regsep  17399  nrmsep3  17420  1stcclb  17508  2ndc1stc  17515  2ndcctbss  17519  2ndcdisj  17520  llyi  17538  nllyi  17539  hausmapdom  17564  elkgen  17569  txbas  17600  txcls  17637  txcnpi  17641  ptpjopn  17645  txdis1cn  17668  txtube  17673  txcmplem1  17674  hausdiag  17678  tx1stc  17683  txkgen  17685  xkococnlem  17692  xkococn  17693  elqtop  17730  kqreglem1  17774  elmptrab  17860  isfbas  17862  elflim2  17997  elflim  18004  hauspwpwf1  18020  alexsublem  18076  ghmcnp  18145  divstgplem  18151  tsmssubm  18173  elutop  18264  ustuqtop4  18275  isucn  18309  iscfilu  18319  ispsmet  18336  ismet  18354  isxmet  18355  ismet2  18364  imasdsf1olem  18404  blres  18462  elmopn  18473  mopni  18523  neibl  18532  nrmmetd  18623  ngppropd  18679  elcncf  18920  mulc1cncf  18936  elpi1  19071  metcld2  19260  pmltpclem1  19346  ovolval  19371  itg1climres  19607  itg2val  19621  isibl  19658  itgeq1f  19664  itgresr  19671  iblcn  19691  itgfsum  19719  dvreslem  19797  dvfsumlem2  19912  pf1ind  19976  deg1ldg  20016  vieta1  20230  ulm2  20302  sincosq2sgn  20408  sincosq4sgn  20410  efopn  20550  dvdsflsumcom  20974  fsumvma2  20999  logfac2  21002  dchrptlem1  21049  lgsdchrval  21132  pntibndlem3  21287  pntlemi  21299  pntleme  21303  pnt3  21307  usgra2edg  21403  trls  21537  istrl2  21539  trlon  21541  is2wlk  21566  spths  21568  0spth  21572  pthon  21576  spthon  21583  isspthonpth  21585  0crct  21614  0cycl  21615  usgrcyclnl2  21629  eupath2lem2  21701  drngoi  21996  rngosn3  22015  vci  22028  isvclem  22057  nmoofval  22264  isph  22324  norm3lemt  22655  isch2  22727  cmbr  23087  eigre  23339  eigorth  23342  nmopub  23412  nmfnleub  23429  cvbr  23786  mdbr  23798  dmdbr  23803  chrelat2  23874  mdsymlem2  23908  rexunirn  23979  ifeqeqx  24002  funcnvmptOLD  24083  funcnvmpt  24084  1stpreima  24096  gsumpropd2lem  24221  isofld  24236  ofldadd  24239  ofldmul  24240  dya2iocuni  24634  itgeq12dv  24642  isrrvv  24702  kur14  24903  pconcn  24912  cnpcon  24918  txpcon  24920  cvmscbv  24946  cvmcov  24951  cvmsi  24953  cvmsval  24954  cvmopnlem  24966  cvmlift2lem10  25000  cvmlift3lem2  25008  cvmlift3lem6  25012  cvmlift3lem7  25013  cvmlift3lem9  25015  cvmlift3  25016  relexp0  25130  relexpsucr  25131  relexpsucl  25133  relexpcnv  25134  relexpdm  25136  relexprn  25137  relexpadd  25139  relexpindlem  25140  rtrclreclem.trans  25147  rtrclreclem.min  25148  prodeq1f  25235  fprod2dlem  25305  eldm3  25386  opelco3  25404  dfon2lem6  25416  dfon2lem7  25417  dfon2lem8  25418  dfon2  25420  preduz  25476  poseq  25529  soseq  25530  sltval  25603  nodenselem5  25641  nocvxminlem  25646  elfuns  25761  brcgr  25840  brbtwn2  25845  axsegconlem1  25857  axsegcon  25867  axcontlem10  25913  brofs  25940  5segofs  25941  brifs  25978  ifscgr  25979  brcolinear  25994  lineext  26011  brfs  26014  fscgr  26015  linecgr  26016  btwnconn1lem4  26025  btwnconn1lem8  26029  btwnconn1lem11  26032  btwnconn1lem12  26033  segcon2  26040  brsegle  26043  outsideofeq  26065  funray  26075  funline  26077  fvline  26079  linethru  26088  mblfinlem3  26246  mblfinlem4  26247  mbfresfi  26254  itg2addnclem3  26259  itg2addnc  26260  itg2gt0cn  26261  areacirclem5  26297  trer  26320  finminlem  26322  ivthALT  26339  locfinnei  26383  comppfsc  26388  filnetlem4  26411  cover2  26416  cover2g  26417  fdc  26450  fdc1  26451  heibor1  26520  bfp  26534  isdrngo1  26573  isriscg  26601  isfldidl2  26680  mrefg2  26762  mzpclval  26783  eldiophb  26816  eldioph2lem1  26819  eldioph3  26825  lzenom  26829  diophin  26832  eldiophss  26834  diophrex  26835  eq0rabdioph  26836  pellexlem3  26895  elpell1qr  26911  elpell14qr  26913  elpell1234qr  26915  jm2.27  27080  rmydioph  27086  expdiophlem1  27093  expdioph  27095  pw2f1ocnv  27109  islbs4  27280  islinds3  27282  hbtlem1  27305  hbtlem7  27307  dgraalem  27328  dgraaub  27331  psgnfval  27401  psgnval  27408  2sbc6g  27593  2sbc5g  27594  iotasbc  27597  dropab1  27627  dropab2  27628  dfdfat2  27972  otthg  28065  oprabv  28086  2ffzoeq  28141  wrdeq0  28173  usgra2wlkspthlem1  28307  spthdifv  28310  usgra2pth  28312  el2wlkonotot0  28340  2spontn0vne  28355  3cyclfrgrarn1  28403  4cycl2vnunb  28408  frg2wot1  28447  usg2spot2nb  28455  bnj956  29148  bnj1146  29163  bnj18eq1  29299  drsb1NEW7  29507  islshpat  29816  lcvbr  29820  lshpsmreu  29908  ldual1dim  29965  cvrval  30068  cvrnbtwn3  30075  iscvlat2N  30123  ishlat3N  30153  hlrelat5N  30199  3dim0  30255  llnexatN  30319  islpln5  30333  islvol5  30377  pmapjat1  30651  ltrnu  30919  cdleme02N  31020  cdlemg33b  31505  cdlemg33c  31506  dvhb1dimN  31784  dibelval3  31946  dibopelval3  31947  dib1dim  31964  dibglbN  31965  diblsmopel  31970  dicval  31975  dicopelval  31976  dicelval3  31979  dicelval1sta  31986  dihopelvalcpre  32047  dih1dimatlem  32128  dihpN  32135  dihjatcclem4  32220  lpolsetN  32281  mapdpglem3  32474  hdmapglem7a  32729
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator