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

Theorem anbi1d 704
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 25 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32rd 640 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  706  anbi12d  710  bi2anan9  873  pm5.71  936  cador  1446  drsb1  2104  eleq1d  2512  eleq1OLD  2517  rexeqf  3037  reueq1f  3038  rmoeq1f  3039  rabeqf  3088  vtocl2gaf  3160  vtocl4ga  3165  alexeqg  3214  alexeq  3215  elrabi  3240  reu2eqd  3282  sbc2or  3322  sbc5  3338  rexss  3552  psstr  3593  ineq1  3678  difin2  3745  r19.28z  3907  r19.28zv  3910  rabsnifsb  4083  ssunsn2  4174  preq12bg  4194  prel12g  4195  opeq1  4202  eluni  4237  csbuni  4262  disjxun  4435  mpteq12f  4513  axrep1  4549  axrep2  4550  axrep3  4551  zfrepclf  4554  axsep  4557  axsep2  4559  zfauscl  4560  reusv2lem4  4641  rabxfrd  4658  opthg  4712  otthg  4720  copsexg  4722  copsexgOLD  4723  euotd  4738  elopab  4745  pocl  4797  dflim2  4924  xpeq1  5003  elxpi  5005  vtoclr  5034  opbrop  5069  opelresg  5271  resopab2  5312  fun11  5643  feq2  5704  f1eq2  5767  f1eq3  5768  foeq2  5782  brprcneu  5849  ssimaexg  5924  dmfco  5932  fndmdif  5976  rexsuppOLD  5997  respreima  6001  isoeq5  6204  isoini  6219  isopolem  6226  f1oiso  6232  f1oiso2  6233  riotaeqdv  6243  oprabid  6308  oprabv  6330  mpt2eq123  6341  mpt2eq123dva  6343  eloprabga  6374  resoprab  6383  resoprab2  6384  elrnmpt2res  6401  ov  6407  ov3  6424  ov6g  6425  ovg  6426  caoftrn  6560  uniuni  6594  limuni3  6672  elxp4  6729  elxp5  6730  opabex3d  6763  opabex3  6764  opiota  6844  eloprabi  6847  cnvf1o  6884  frxp  6895  xporderlem  6896  poxp  6897  fnwelem  6900  suppimacnv  6914  rexsupp  6920  mpt2curryd  7000  smoel2  7036  omeu  7236  oeeui  7253  omabs  7298  omopth  7309  qliftel  7396  brecop  7406  eroveu  7408  erov  7410  ecopovtrn  7416  ixpsnf1o  7511  dom2lem  7557  xpsnen  7603  xpassen  7613  pw2f1olem  7623  xpf1o  7681  unxpdom  7729  domunfican  7795  preleq  8037  zfinf  8059  cantnfs  8088  cantnfsOLD  8118  tcvalg  8172  r0weon  8393  fseqenlem1  8408  acni2  8430  aceq1  8501  aceq0  8502  dfac2a  8513  dfac12lem2  8527  cardcf  8635  cfeq0  8639  cfsuc  8640  cff1  8641  cfss  8648  isf32lem5  8740  fin1a2lem6  8788  zfac  8843  brdom7disj  8912  brdom6disj  8913  axrepnd  8972  axunndlem1  8973  axinfnd  8987  axacndlem5  8992  axacnd  8993  zfcndrep  8995  zfcndinf  8999  zfcndac  9000  pwfseqlem4a  9042  pwfseqlem4  9043  gruina  9199  grothomex  9210  ordpipq  9323  elnpi  9369  genpass  9390  ltprord  9411  reclem2pr  9429  reclem3pr  9430  recexpr  9432  addsrmo  9453  mulsrmo  9454  addsrpr  9455  mulsrpr  9456  ltsosr  9474  mulgt0sr  9485  supsr  9492  ltresr  9520  axpre-lttrn  9546  axpre-mulgt0  9548  prime  10949  peano5uzti  10958  uzindOLD  10963  rexuz  11140  ltxr  11333  qbtwnre  11407  xmulneg1  11470  supxr2  11514  ixxval  11546  fzval  11683  nn0opth2  12331  hashbclem  12480  hashf1lem2  12484  eqwrd  12561  swrdeq  12650  wrd2ind  12682  cshwcsh2id  12775  abslt  13126  absle  13127  lenegsq  13132  abs2difabs  13146  ello12  13318  elo12  13329  o1lo1  13339  rlimuni  13352  lo1resb  13366  o1resb  13368  2clim  13374  rlimcn2  13392  climcn2  13394  addcn2  13395  mulcn2  13397  o1of2  13414  sumeq1  13490  fsum2dlem  13564  modfsummod  13587  znnenlem  13822  nndivdvds  13869  divalg2  13940  smupval  14015  gcdval  14023  gcdass  14060  rpexp  14138  pythagtriplem2  14218  pythagtrip  14235  vdwapun  14369  0ram  14415  ramub1lem2  14422  pwsle  14766  imasleval  14815  ismre  14864  ismri  14905  iscatd2  14955  isssc  15066  funcpropd  15143  fullpropd  15163  fthres2b  15173  fthres2c  15174  setcsect  15290  prslem  15434  drsdir  15438  posi  15453  tosso  15540  ipoval  15658  ipolt  15663  odudlatb  15700  dirge  15741  gsumpropd2lem  15774  issgrpv  15787  issgrpn0  15788  mhmpropd  15846  mrcmndind  15871  mgmnsgrpex  15923  issubg3  16093  isga  16203  symgfixelq  16332  psgnfval  16399  psgnval  16406  isslw  16502  dprdw  16917  dprdwOLD  16924  subgdmdprd  16955  drngpropd  17297  issubrg  17303  islmod  17390  lmodlema  17391  lmodprop2d  17446  lsslss  17481  lbspropd  17619  lbsacsbs  17676  aspval2  17870  psrbag  17887  pf1ind  18265  znleval  18466  islbs4  18740  islinds3  18742  mdetunilem4  18990  mdetunilem9  18995  istopg  19277  basis2  19325  tg2  19339  iscld  19401  neival  19476  isnei  19477  isneip  19479  neiptoptop  19505  neiptopnei  19506  neitr  19554  restlp  19557  iscn  19609  cnpval  19610  iscnp  19611  regsep  19708  nrmsep3  19729  1stcclb  19818  2ndc1stc  19825  2ndcctbss  19829  2ndcdisj  19830  llyi  19848  nllyi  19849  hausmapdom  19874  locfinnei  19897  comppfsc  19906  elkgen  19910  txbas  19941  txcls  19978  txcnpi  19982  ptpjopn  19986  txdis1cn  20009  txtube  20014  txcmplem1  20015  hausdiag  20019  tx1stc  20024  txkgen  20026  xkococnlem  20033  xkococn  20034  elqtop  20071  kqreglem1  20115  elmptrab  20201  isfbas  20203  elflim2  20338  elflim  20345  hauspwpwf1  20361  alexsublem  20417  ghmcnp  20486  qustgplem  20492  tsmssubm  20517  elutop  20609  ustuqtop4  20620  isucn  20654  iscfilu  20664  ispsmet  20681  ismet  20699  isxmet  20700  ismet2  20709  imasdsf1olem  20749  blres  20807  elmopn  20818  mopni  20868  neibl  20877  nrmmetd  20968  ngppropd  21024  elcncf  21266  mulc1cncf  21282  elpi1  21418  metcld2  21618  pmltpclem1  21733  ovolval  21758  itg1climres  21994  itg2val  22008  isibl  22045  itgeq1f  22051  itgresr  22058  iblcn  22078  itgfsum  22106  dvreslem  22186  dvfsumlem2  22301  deg1ldg  22365  vieta1  22580  ulm2  22652  sincosq2sgn  22764  sincosq4sgn  22766  efopn  22911  dvdsflsumcom  23336  fsumvma2  23361  logfac2  23364  dchrptlem1  23411  lgsdchrval  23494  pntibndlem3  23649  pntlemi  23661  pntleme  23665  pnt3  23669  istrkg2d  23728  istrkgld  23729  istrkg2ld  23730  axtgsegcon  23733  axtg5seg  23734  axtgpasch  23736  axtgupdim2  23741  legov  23844  islnopp  23985  ishpg  24000  brcgr  24075  brbtwn2  24080  axsegconlem1  24092  axsegcon  24102  axcontlem10  24148  usgra2edg  24254  trls  24410  istrl2  24412  trlon  24414  is2wlk  24439  spths  24441  0spth  24445  pthon  24449  spthon  24456  isspthonpth  24458  usgra2wlkspthlem1  24491  0crct  24498  0cycl  24499  usgrcyclnl2  24513  wwlknprop  24558  vfwlkniswwlkn  24578  wwlknext  24596  wwlknfi  24610  clwlk  24625  isclwlk  24628  clwlkcompim  24636  clwwlkn2  24647  clwwlknimp  24648  clwwlkel  24665  clwwlkf  24666  clwwlkext2edg  24674  wwlkext2clwwlk  24675  wwlksubclwwlk  24676  erclwwlknsym  24698  erclwwlkntr  24699  clwlkfoclwwlk  24717  el2wlkonotot0  24744  2spontn0vne  24759  rusgranumwlkl1  24819  rusgranumwlklem3  24823  rusgranumwlkb0  24825  rusgra0edg  24827  eupath2lem2  24850  3cyclfrgrarn1  24884  4cycl2vnunb  24889  frg2wot1  24929  usg2spot2nb  24937  extwwlkfablem2  24950  numclwwlkovfel2  24955  numclwwlkovf2  24956  numclwwlkovf2ex  24958  numclwwlkovgel  24960  numclwwlkovgelim  24961  numclwlk2lem2f  24975  numclwlk2lem2f1o  24977  numclwwlk5  24984  drngoi  25281  rngosn3  25300  vci  25313  isvclem  25342  nmoofval  25549  isph  25609  norm3lemt  25941  isch2  26013  cmbr  26374  eigre  26626  eigorth  26629  nmopub  26699  nmfnleub  26716  cvbr  27073  mdbr  27085  dmdbr  27090  chrelat2  27161  mdsymlem2  27195  rexunirn  27262  ifeqeqx  27291  funcnvmptOLD  27381  funcnvmpt  27382  1stpreima  27396  fpwrelmapffslem  27427  isomnd  27564  archirng  27605  isslmd  27618  slmdlema  27619  orngmul  27666  dya2iocuni  28127  omsfval  28138  itgeq12dv  28141  isrrvv  28255  brafs  28425  kur14  28533  pconcn  28542  cnpcon  28548  txpcon  28550  cvmscbv  28576  cvmcov  28581  cvmsi  28583  cvmsval  28584  cvmopnlem  28596  cvmlift2lem10  28630  cvmlift3lem2  28638  cvmlift3lem6  28642  cvmlift3lem7  28643  cvmlift3lem9  28645  cvmlift3  28646  mclsssvlem  28795  mclsind  28803  relexp0  28925  relexpsucr  28926  relexpsucl  28928  relexpcnv  28929  relexpdm  28931  relexprn  28932  relexpadd  28934  relexpindlem  28935  rtrclreclem.trans  28942  rtrclreclem.min  28943  prodeq1f  29015  fprod2dlem  29085  eldm3  29166  opelco3  29183  dfon2lem6  29195  dfon2lem7  29196  dfon2lem8  29197  dfon2  29199  preduz  29255  poseq  29308  soseq  29309  sltval  29382  nodenselem5  29420  nocvxminlem  29425  elfuns  29540  brofs  29630  5segofs  29631  brifs  29668  ifscgr  29669  brcolinear  29684  lineext  29701  brfs  29704  fscgr  29705  linecgr  29706  btwnconn1lem4  29715  btwnconn1lem8  29719  btwnconn1lem11  29722  btwnconn1lem12  29723  segcon2  29730  brsegle  29733  outsideofeq  29755  funray  29765  funline  29767  fvline  29769  linethru  29778  wl-ax11-lem8  30007  ptrest  30023  heicant  30024  mblfinlem3  30028  mblfinlem4  30029  mbfresfi  30036  itg2addnclem3  30043  itg2addnc  30044  itg2gt0cn  30045  areacirclem5  30086  trer  30109  finminlem  30111  ivthALT  30128  filnetlem4  30174  cover2  30179  cover2g  30180  fdc  30213  fdc1  30214  heibor1  30281  bfp  30295  isdrngo1  30334  isriscg  30362  isfldidl2  30441  mrefg2  30614  mzpclval  30632  eldiophb  30665  eldioph2lem1  30668  eldioph3  30674  lzenom  30678  diophin  30681  eldiophss  30683  diophrex  30684  eq0rabdioph  30685  pellexlem3  30742  elpell1qr  30758  elpell14qr  30760  elpell1234qr  30762  jm2.27  30925  rmydioph  30931  expdiophlem1  30938  expdioph  30940  pw2f1ocnv  30954  hbtlem1  31047  hbtlem7  31049  dgraalem  31070  dgraaub  31073  lcmval  31174  lcmass  31194  2sbc6g  31276  2sbc5g  31277  iotasbc  31280  dropab1  31310  dropab2  31311  mullimc  31530  mullimcf  31537  fourierdlem42  31820  fourierdlem48  31826  fourierdlem50  31828  fourierdlem51  31829  fourierdlem54  31832  fourierdlem86  31864  dfdfat2  32054  2ffzoeq  32179  spthdifv  32190  usgra2pth  32192  edgssv2ALT  32239  edgssv2  32240  isfusgra0  32263  fusgraimpclALT2  32269  mgmhmpropd  32311  isrnghm  32416  rngcsect  32528  rngcinv  32529  rngcsectOLD  32540  rngcinvOLD  32541  ringcsect  32576  ringcinv  32577  ringcsectOLD  32600  ringcinvOLD  32601  lmod1  32828  bnj956  33568  bnj1146  33583  bnj18eq1  33718  bj-axrep1  34122  bj-axrep2  34123  bj-axrep3  34124  bj-axsep  34127  bj-eleq1w  34170  bj-rabeqd  34236  bj-axsep2  34241  islshpat  34482  lcvbr  34486  lshpsmreu  34574  ldual1dim  34631  cvrval  34734  cvrnbtwn3  34741  iscvlat2N  34789  ishlat3N  34819  hlrelat5N  34865  3dim0  34921  llnexatN  34985  islpln5  34999  islvol5  35043  pmapjat1  35317  ltrnu  35585  cdleme02N  35687  cdlemg33b  36173  cdlemg33c  36174  dvhb1dimN  36452  dibelval3  36614  dibopelval3  36615  dib1dim  36632  dibglbN  36633  diblsmopel  36638  dicval  36643  dicopelval  36644  dicelval3  36647  dicelval1sta  36654  dihopelvalcpre  36715  dih1dimatlem  36796  dihpN  36803  dihjatcclem4  36888  lpolsetN  36949  mapdpglem3  37142  hdmapglem7a  37397
  Copyright terms: Public domain W3C validator