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  2116  eleq1  2502  rexeqf  2907  reueq1f  2908  rmoeq1f  2909  rabeqf  2955  vtocl2gaf  3024  alexeq  3071  ceqex  3072  elrabi  3096  sbc2or  3175  sbc5  3191  rexss  3396  psstr  3437  ineq1  3521  difin2  3588  r19.28z  3744  r19.28zv  3747  ssunsn2  3982  preq12bg  4001  opeq1  4008  eluni  4042  disjxun  4235  mpteq12f  4310  axrep1  4346  axrep2  4347  axrep3  4348  zfrepclf  4351  axsep  4354  axsep2  4356  zfauscl  4357  opthg  4465  copsexg  4471  euotd  4486  elopab  4491  pocl  4539  dflim2  4666  uniuni  4745  reusv2lem4  4756  rabxfrd  4773  limuni3  4861  xpeq1  4921  elxpi  4923  vtoclr  4951  opbrop  4984  opelresg  5182  resopab2  5219  elxp4  5386  elxp5  5387  fun11  5545  feq2  5606  f1eq2  5664  f1eq3  5665  foeq2  5679  brprcneu  5750  ssimaexg  5818  dmfco  5826  fndmdif  5863  rexsupp  5884  respreima  5888  opabex3d  6018  opabex3  6019  isoeq5  6072  isoini  6087  isopolem  6094  f1oiso  6100  f1oiso2  6101  oprabid  6134  mpt2eq123  6162  mpt2eq123dva  6164  eloprabga  6189  resoprab  6195  resoprab2  6196  ov  6222  ov3  6239  ov6g  6240  ovg  6241  caoftrn  6368  eloprabi  6442  cnvf1o  6474  frxp  6485  xporderlem  6486  poxp  6487  fnwelem  6490  opiota  6564  riotaeqdv  6579  smoel2  6654  omeu  6857  oeeui  6874  omabs  6919  omopth  6930  qliftel  7016  brecop  7026  eroveu  7028  erov  7030  ecopovtrn  7036  th3qlem2  7040  th3q  7042  ixpsnf1o  7131  dom2lem  7176  xpsnen  7221  xpassen  7231  pw2f1olem  7241  xpf1o  7298  unxpdom  7345  domunfican  7408  preleq  7601  zfinf  7623  cantnfs  7650  tcvalg  7706  r0weon  7925  fseqenlem1  7936  acni2  7958  aceq1  8029  aceq0  8030  dfac2a  8041  dfac12lem2  8055  cardcf  8163  cfeq0  8167  cfsuc  8168  cff1  8169  cfss  8176  isf32lem5  8268  fin1a2lem6  8316  zfac  8371  brdom7disj  8440  brdom6disj  8441  axrepnd  8500  axunndlem1  8501  axinfnd  8512  axacndlem5  8517  axacnd  8518  zfcndrep  8520  zfcndinf  8524  zfcndac  8525  pwfseqlem4a  8567  pwfseqlem4  8568  gruina  8724  grothomex  8735  ordpipq  8850  elnpi  8896  genpass  8917  ltprord  8938  reclem2pr  8956  reclem3pr  8957  recexpr  8959  ltsosr  9000  mulgt0sr  9011  supsr  9018  ltresr  9046  axpre-lttrn  9072  axpre-mulgt0  9074  prime  10381  peano5uzti  10390  uzindOLD  10395  rexuz  10558  ltxr  10746  qbtwnre  10816  xmulneg1  10879  supxr2  10923  ixxval  10955  fzval  11076  nn0opth2  11596  hashbclem  11732  hashf1lem2  11736  abslt  12149  absle  12150  lenegsq  12155  abs2difabs  12169  ello12  12341  elo12  12352  o1lo1  12362  rlimuni  12375  lo1resb  12389  o1resb  12391  2clim  12397  rlimcn2  12415  climcn2  12417  addcn2  12418  mulcn2  12420  o1of2  12437  sumeq1f  12513  fsum2dlem  12585  znnenlem  12842  nndivdvds  12889  divalg2  12956  smupval  13031  gcdval  13039  gcdass  13076  rpexp  13151  pythagtriplem2  13222  pythagtrip  13239  vdwapun  13373  0ram  13419  ramub1lem2  13426  pwsle  13745  imasleval  13797  ismre  13846  ismri  13887  iscatd2  13937  isssc  14051  funcpropd  14128  fullpropd  14148  fthres2b  14158  fthres2c  14159  setcsect  14275  prslem  14419  drsdir  14423  posi  14438  tosso  14496  ipoval  14611  ipolt  14616  odudlatb  14653  dirge  14713  mndpropd  14752  mhmpropd  14775  issubg3  14991  isga  15099  isslw  15273  dprdw  15599  subgdmdprd  15623  drngpropd  15893  issubrg  15899  islmod  15985  lmodlema  15986  lmodprop2d  16037  lsslss  16068  lbspropd  16202  lbsacsbs  16259  aspval2  16436  psrbag  16462  znleval  16866  istopg  16999  basis2  17047  tg2  17061  iscld  17122  neival  17197  isnei  17198  isneip  17200  neiptoptop  17226  neiptopnei  17227  neitr  17275  restlp  17278  iscn  17330  cnpval  17331  iscnp  17332  regsep  17429  nrmsep3  17450  1stcclb  17538  2ndc1stc  17545  2ndcctbss  17549  2ndcdisj  17550  llyi  17568  nllyi  17569  hausmapdom  17594  elkgen  17599  txbas  17630  txcls  17667  txcnpi  17671  ptpjopn  17675  txdis1cn  17698  txtube  17703  txcmplem1  17704  hausdiag  17708  tx1stc  17713  txkgen  17715  xkococnlem  17722  xkococn  17723  elqtop  17760  kqreglem1  17804  elmptrab  17890  isfbas  17892  elflim2  18027  elflim  18034  hauspwpwf1  18050  alexsublem  18106  ghmcnp  18175  divstgplem  18181  tsmssubm  18203  elutop  18294  ustuqtop4  18305  isucn  18339  iscfilu  18349  ispsmet  18366  ismet  18384  isxmet  18385  ismet2  18394  imasdsf1olem  18434  blres  18492  elmopn  18503  mopni  18553  neibl  18562  nrmmetd  18653  ngppropd  18709  elcncf  18950  mulc1cncf  18966  elpi1  19101  metcld2  19290  pmltpclem1  19376  ovolval  19401  itg1climres  19635  itg2val  19649  isibl  19686  itgeq1f  19692  itgresr  19699  iblcn  19719  itgfsum  19747  dvreslem  19827  dvfsumlem2  19942  pf1ind  20006  deg1ldg  20046  vieta1  20260  ulm2  20332  sincosq2sgn  20438  sincosq4sgn  20440  efopn  20580  dvdsflsumcom  21004  fsumvma2  21029  logfac2  21032  dchrptlem1  21079  lgsdchrval  21162  pntibndlem3  21317  pntlemi  21329  pntleme  21333  pnt3  21337  usgra2edg  21433  trls  21567  istrl2  21569  trlon  21571  is2wlk  21596  spths  21598  0spth  21602  pthon  21606  spthon  21613  isspthonpth  21615  0crct  21644  0cycl  21645  usgrcyclnl2  21659  eupath2lem2  21731  drngoi  22026  rngosn3  22045  vci  22058  isvclem  22087  nmoofval  22294  isph  22354  norm3lemt  22685  isch2  22757  cmbr  23117  eigre  23369  eigorth  23372  nmopub  23442  nmfnleub  23459  cvbr  23816  mdbr  23828  dmdbr  23833  chrelat2  23904  mdsymlem2  23938  rexunirn  24009  ifeqeqx  24032  funcnvmptOLD  24113  funcnvmpt  24114  1stpreima  24126  gsumpropd2lem  24251  isofld  24266  ofldadd  24269  ofldmul  24270  dya2iocuni  24664  itgeq12dv  24672  isrrvv  24732  kur14  24933  pconcn  24942  cnpcon  24948  txpcon  24950  cvmscbv  24976  cvmcov  24981  cvmsi  24983  cvmsval  24984  cvmopnlem  24996  cvmlift2lem10  25030  cvmlift3lem2  25038  cvmlift3lem6  25042  cvmlift3lem7  25043  cvmlift3lem9  25045  cvmlift3  25046  relexp0  25160  relexpsucr  25161  relexpsucl  25163  relexpcnv  25164  relexpdm  25166  relexprn  25167  relexpadd  25169  relexpindlem  25170  rtrclreclem.trans  25177  rtrclreclem.min  25178  prodeq1f  25265  fprod2dlem  25335  eldm3  25416  opelco3  25434  dfon2lem6  25446  dfon2lem7  25447  dfon2lem8  25448  dfon2  25450  preduz  25506  poseq  25559  soseq  25560  sltval  25633  nodenselem5  25671  nocvxminlem  25676  elfuns  25791  brcgr  25870  brbtwn2  25875  axsegconlem1  25887  axsegcon  25897  axcontlem10  25943  brofs  25970  5segofs  25971  brifs  26008  ifscgr  26009  brcolinear  26024  lineext  26041  brfs  26044  fscgr  26045  linecgr  26046  btwnconn1lem4  26055  btwnconn1lem8  26059  btwnconn1lem11  26062  btwnconn1lem12  26063  segcon2  26070  brsegle  26073  outsideofeq  26095  funray  26105  funline  26107  fvline  26109  linethru  26118  heicant  26277  mblfinlem3  26281  mblfinlem4  26282  mbfresfi  26289  itg2addnclem3  26296  itg2addnc  26297  itg2gt0cn  26298  areacirclem5  26334  trer  26357  finminlem  26359  ivthALT  26376  locfinnei  26420  comppfsc  26425  filnetlem4  26448  cover2  26453  cover2g  26454  fdc  26487  fdc1  26488  heibor1  26557  bfp  26571  isdrngo1  26610  isriscg  26638  isfldidl2  26717  mrefg2  26799  mzpclval  26820  eldiophb  26853  eldioph2lem1  26856  eldioph3  26862  lzenom  26866  diophin  26869  eldiophss  26871  diophrex  26872  eq0rabdioph  26873  pellexlem3  26932  elpell1qr  26948  elpell14qr  26950  elpell1234qr  26952  jm2.27  27117  rmydioph  27123  expdiophlem1  27130  expdioph  27132  pw2f1ocnv  27146  islbs4  27317  islinds3  27319  hbtlem1  27342  hbtlem7  27344  dgraalem  27365  dgraaub  27368  psgnfval  27438  psgnval  27445  2sbc6g  27630  2sbc5g  27631  iotasbc  27634  dropab1  27664  dropab2  27665  dfdfat2  28009  otthg  28103  oprabv  28127  2ffzoeq  28187  wrdeq0  28228  usgra2wlkspthlem1  28368  spthdifv  28371  usgra2pth  28373  wwlknprop  28392  el2wlkonotot0  28428  2spontn0vne  28443  3cyclfrgrarn1  28500  4cycl2vnunb  28505  frg2wot1  28544  usg2spot2nb  28552  bnj956  29245  bnj1146  29260  bnj18eq1  29396  drsb1NEW7  29604  islshpat  29913  lcvbr  29917  lshpsmreu  30005  ldual1dim  30062  cvrval  30165  cvrnbtwn3  30172  iscvlat2N  30220  ishlat3N  30250  hlrelat5N  30296  3dim0  30352  llnexatN  30416  islpln5  30430  islvol5  30474  pmapjat1  30748  ltrnu  31016  cdleme02N  31117  cdlemg33b  31602  cdlemg33c  31603  dvhb1dimN  31881  dibelval3  32043  dibopelval3  32044  dib1dim  32061  dibglbN  32062  diblsmopel  32067  dicval  32072  dicopelval  32073  dicelval3  32076  dicelval1sta  32083  dihopelvalcpre  32144  dih1dimatlem  32225  dihpN  32232  dihjatcclem4  32317  lpolsetN  32378  mapdpglem3  32571  hdmapglem7a  32826
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 179  df-an 362
  Copyright terms: Public domain W3C validator