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  1506  drsb1  2172  eleq1d  2498  eleq1OLD  2503  rexeqf  3029  reueq1f  3030  rmoeq1f  3031  rabeqf  3080  vtocl2gaf  3152  vtocl4ga  3157  alexeqg  3206  alexeq  3207  elrabi  3232  reu2eqd  3274  sbc2or  3314  sbc5  3330  rexss  3534  psstr  3575  ineq1  3663  difin2  3741  r19.28z  3895  r19.28zv  3898  rabsnifsb  4071  ssunsn2  4162  preq12bg  4182  prel12g  4183  opeq1  4190  eluni  4225  csbuni  4250  disjxun  4424  mpteq12f  4502  axrep1  4539  axrep2  4540  axrep3  4541  zfrepclf  4544  axsep  4547  axsep2  4549  zfauscl  4550  reusv2lem4  4629  rabxfrd  4643  opthg  4697  otthg  4705  copsexg  4707  euotd  4722  elopab  4729  pocl  4782  xpeq1  4868  elxpi  4870  vtoclr  4899  opbrop  4934  opelresg  5132  resopab2  5173  dflim2  5498  fun11  5666  feq2  5729  f1eq2  5792  f1eq3  5793  foeq2  5807  brprcneu  5874  ssimaexg  5947  dmfco  5955  fndmdif  6001  respreima  6024  isoeq5  6229  isoini  6244  isopolem  6251  f1oiso  6257  f1oiso2  6258  riotaeqdv  6268  oprabid  6332  oprabv  6353  mpt2eq123  6364  mpt2eq123dva  6366  eloprabga  6397  resoprab  6406  resoprab2  6407  elrnmpt2res  6424  ov  6430  ov3  6447  ov6g  6448  ovg  6449  caoftrn  6580  uniuni  6614  limuni3  6693  elxp4  6751  elxp5  6752  opabex3d  6785  opabex3  6786  opiota  6866  eloprabi  6869  cnvf1o  6906  frxp  6917  xporderlem  6918  poxp  6919  fnwelem  6922  suppimacnv  6936  rexsupp  6944  mpt2curryd  7024  smoel2  7090  omeu  7294  oeeui  7311  omabs  7356  omopth  7367  qliftel  7454  brecop  7464  eroveu  7466  erov  7468  ecopovtrn  7474  ixpsnf1o  7570  dom2lem  7616  xpsnen  7662  xpassen  7672  pw2f1olem  7682  xpf1o  7740  unxpdom  7785  domunfican  7850  preleq  8122  zfinf  8144  cantnfs  8170  tcvalg  8221  r0weon  8442  fseqenlem1  8453  acni2  8475  aceq1  8546  aceq0  8547  dfac2a  8558  dfac12lem2  8572  cardcf  8680  cfeq0  8684  cfsuc  8685  cff1  8686  cfss  8693  isf32lem5  8785  fin1a2lem6  8833  zfac  8888  brdom7disj  8957  brdom6disj  8958  axrepnd  9017  axunndlem1  9018  axinfnd  9030  axacndlem5  9035  axacnd  9036  zfcndrep  9038  zfcndinf  9042  zfcndac  9043  pwfseqlem4a  9085  pwfseqlem4  9086  gruina  9242  grothomex  9253  ordpipq  9366  elnpi  9412  genpass  9433  ltprord  9454  reclem2pr  9472  reclem3pr  9473  recexpr  9475  addsrmo  9496  mulsrmo  9497  addsrpr  9498  mulsrpr  9499  ltsosr  9517  mulgt0sr  9528  supsr  9535  ltresr  9563  axpre-lttrn  9589  axpre-mulgt0  9591  prime  11016  peano5uzti  11025  rexuz  11209  ltxr  11415  qbtwnre  11492  xmulneg1  11555  supxr2  11599  ixxval  11643  fzval  11784  preduz  11909  nn0opth2  12455  hashbclem  12610  hashf1lem2  12614  eqwrd  12695  swrdeq  12785  wrd2ind  12819  cshwcsh2id  12912  cleq1lem  13025  rtrclreclem3  13102  rtrclreclem4  13103  relexpindlem  13105  abslt  13356  absle  13357  lenegsq  13362  abs2difabs  13376  ello12  13558  elo12  13569  o1lo1  13579  rlimuni  13592  lo1resb  13606  o1resb  13608  2clim  13614  rlimcn2  13632  climcn2  13634  addcn2  13635  mulcn2  13637  o1of2  13654  sumeq1  13733  fsum2dlem  13809  modfsummod  13832  prodeq1f  13940  fprod2dlem  14012  znnenlem  14242  nndivdvds  14289  divalg2  14361  smupval  14436  gcdval  14444  gcdass  14484  lcmval  14522  lcmass  14544  rpexp  14634  pythagtriplem2  14721  pythagtrip  14738  vdwapun  14878  0ram  14932  ramub1lem2  14939  pwsle  15340  imasleval  15389  ismre  15438  ismri  15479  iscatd2  15529  dfiso2  15619  isssc  15667  funcpropd  15747  fullpropd  15767  fthres2b  15777  fthres2c  15778  setcsect  15926  prslem  16118  drsdir  16122  posi  16137  tosso  16224  ipoval  16342  ipolt  16347  odudlatb  16384  dirge  16425  gsumpropd2lem  16458  issgrpv  16471  issgrpn0  16472  mhmpropd  16530  mrcmndind  16555  mgmnsgrpex  16607  issubg3  16777  isga  16887  symgfixelq  17016  psgnfval  17083  psgnval  17090  isslw  17186  dprdw  17568  subgdmdprd  17593  drngpropd  17928  issubrg  17934  islmod  18021  lmodlema  18022  lmodprop2d  18076  lsslss  18110  lbspropd  18248  lbsacsbs  18305  aspval2  18497  psrbag  18514  pf1ind  18869  znleval  19047  islbs4  19312  islinds3  19314  mdetunilem4  19562  mdetunilem9  19567  istopg  19847  basis2  19888  tg2  19902  iscld  19964  neival  20040  isnei  20041  isneip  20043  neiptoptop  20069  neiptopnei  20070  neitr  20118  restlp  20121  iscn  20173  cnpval  20174  iscnp  20175  regsep  20272  nrmsep3  20293  1stcclb  20381  2ndc1stc  20388  2ndcctbss  20392  2ndcdisj  20393  llyi  20411  nllyi  20412  hausmapdom  20437  locfinnei  20460  comppfsc  20469  elkgen  20473  txbas  20504  txcls  20541  txcnpi  20545  ptpjopn  20549  txdis1cn  20572  txtube  20577  txcmplem1  20578  hausdiag  20582  tx1stc  20587  txkgen  20589  xkococnlem  20596  xkococn  20597  elqtop  20634  kqreglem1  20678  elmptrab  20764  isfbas  20766  elflim2  20901  elflim  20908  hauspwpwf1  20924  alexsublem  20981  ghmcnp  21051  qustgplem  21057  tsmssubm  21079  elutop  21170  ustuqtop4  21181  isucn  21215  iscfilu  21225  ispsmet  21242  ismet  21260  isxmet  21261  ismet2  21270  imasdsf1olem  21310  blres  21368  elmopn  21379  mopni  21429  neibl  21438  nrmmetd  21511  ngppropd  21567  elcncf  21808  mulc1cncf  21824  elpi1  21960  metcld2  22160  pmltpclem1  22271  ovolval  22296  itg1climres  22540  itg2val  22554  isibl  22591  itgeq1f  22597  itgresr  22604  iblcn  22624  itgfsum  22652  dvreslem  22732  dvfsumlem2  22847  deg1ldg  22909  vieta1  23124  ulm2  23196  sincosq2sgn  23310  sincosq4sgn  23312  efopn  23459  dvdsflsumcom  23971  fsumvma2  23996  logfac2  23999  dchrptlem1  24046  lgsdchrval  24129  pntibndlem3  24284  pntlemi  24296  pntleme  24300  pnt3  24304  istrkgld  24361  istrkg2ld  24362  istrkg3ld  24363  axtgsegcon  24366  axtg5seg  24367  axtgpasch  24369  axtgupdim2  24373  legov  24481  islnopp  24629  ishpg  24648  iscgra1  24699  brcgr  24767  brbtwn2  24772  axsegconlem1  24784  axsegcon  24794  axcontlem10  24840  usgra2edg  24946  trls  25102  istrl2  25104  trlon  25106  is2wlk  25131  spths  25133  0spth  25137  pthon  25141  spthon  25148  isspthonpth  25150  usgra2wlkspthlem1  25183  0crct  25190  0cycl  25191  usgrcyclnl2  25205  wwlknprop  25250  vfwlkniswwlkn  25270  wwlknext  25288  wwlknfi  25302  clwlk  25317  isclwlk  25320  clwlkcompim  25328  clwwlkn2  25339  clwwlknimp  25340  clwwlkel  25357  clwwlkf  25358  clwwlkext2edg  25366  wwlkext2clwwlk  25367  wwlksubclwwlk  25368  erclwwlknsym  25390  erclwwlkntr  25391  clwlkfoclwwlk  25409  el2wlkonotot0  25436  2spontn0vne  25451  rusgranumwlkl1  25511  rusgranumwlklem3  25515  rusgranumwlkb0  25517  rusgra0edg  25519  eupath2lem2  25542  3cyclfrgrarn1  25576  4cycl2vnunb  25581  frg2wot1  25621  usg2spot2nb  25629  extwwlkfablem2  25642  numclwwlkovfel2  25647  numclwwlkovf2  25648  numclwwlkovf2ex  25650  numclwwlkovgel  25652  numclwwlkovgelim  25653  numclwlk2lem2f  25667  numclwlk2lem2f1o  25669  numclwwlk5  25676  drngoi  25971  rngosn3  25990  vci  26003  isvclem  26032  nmoofval  26239  isph  26299  norm3lemt  26631  isch2  26702  cmbr  27063  eigre  27314  eigorth  27317  nmopub  27387  nmfnleub  27404  cvbr  27761  mdbr  27773  dmdbr  27778  chrelat2  27849  mdsymlem2  27883  rexunirn  27953  ifeqeqx  27988  funcnvmptOLD  28101  funcnvmpt  28102  1stpreima  28118  fpwrelmapffslem  28151  isomnd  28293  archirng  28334  isslmd  28347  slmdlema  28348  orngmul  28396  dya2iocuni  28935  omsfval  28946  elcarsg  28957  itgeq12dv  28978  isrrvv  29093  istrkg2d  29262  axtgupdim2OLD  29264  brafs  29268  bnj956  29367  bnj1146  29382  bnj18eq1  29517  kur14  29718  pconcn  29726  cnpcon  29732  txpcon  29734  cvmscbv  29760  cvmcov  29765  cvmsi  29767  cvmsval  29768  cvmopnlem  29780  cvmlift2lem10  29814  cvmlift3lem2  29822  cvmlift3lem6  29826  cvmlift3lem7  29827  cvmlift3lem9  29829  cvmlift3  29830  mclsssvlem  29979  mclsind  29987  eldm3  30180  opelco3  30198  fv1stcnv  30200  fv2ndcnv  30201  dfon2lem6  30212  dfon2lem7  30213  dfon2lem8  30214  dfon2  30216  poseq  30269  soseq  30270  sltval  30312  nodenselem5  30350  nocvxminlem  30355  elfuns  30458  brsuccf  30484  brofs  30548  5segofs  30549  brifs  30586  ifscgr  30587  brcolinear  30602  lineext  30619  brfs  30622  fscgr  30623  linecgr  30624  btwnconn1lem4  30633  btwnconn1lem8  30637  btwnconn1lem11  30640  btwnconn1lem12  30641  segcon2  30648  brsegle  30651  outsideofeq  30673  funray  30683  funline  30685  fvline  30687  linethru  30696  trer  30748  finminlem  30750  ivthALT  30767  filnetlem4  30813  bj-axrep1  31145  bj-axrep2  31146  bj-axrep3  31147  bj-axsep  31150  bj-eleq1w  31197  bj-ax8  31236  bj-rabeqd  31264  bj-axsep2  31269  topdifinffinlem  31475  icoreval  31481  isbasisrelowllem1  31483  isbasisrelowllem2  31484  relowlssretop  31491  wl-ax11-lem8  31616  ptrest  31633  poimirlem1  31635  poimirlem13  31647  poimirlem14  31648  poimirlem22  31656  poimirlem24  31658  poimirlem26  31660  poimirlem27  31661  heicant  31669  mblfinlem3  31673  mblfinlem4  31674  mbfresfi  31681  itg2addnclem3  31689  itg2addnc  31690  itg2gt0cn  31691  areacirclem5  31730  cover2  31734  cover2g  31735  fdc  31768  fdc1  31769  heibor1  31836  bfp  31850  isdrngo1  31889  isriscg  31917  isfldidl2  31996  islshpat  32282  lcvbr  32286  lshpsmreu  32374  ldual1dim  32431  cvrval  32534  cvrnbtwn3  32541  iscvlat2N  32589  ishlat3N  32619  hlrelat5N  32665  3dim0  32721  llnexatN  32785  islpln5  32799  islvol5  32843  pmapjat1  33117  ltrnu  33385  cdleme02N  33487  cdlemg33b  33973  cdlemg33c  33974  dvhb1dimN  34252  dibelval3  34414  dibopelval3  34415  dib1dim  34432  dibglbN  34433  diblsmopel  34438  dicval  34443  dicopelval  34444  dicelval3  34447  dicelval1sta  34454  dihopelvalcpre  34515  dih1dimatlem  34596  dihpN  34603  dihjatcclem4  34688  lpolsetN  34749  mapdpglem3  34942  hdmapglem7a  35197  mrefg2  35248  mzpclval  35266  eldiophb  35298  eldioph2lem1  35301  eldioph3  35307  lzenom  35311  diophin  35314  eldiophss  35316  diophrex  35317  eq0rabdioph  35318  pellexlem3  35375  elpell1qr  35391  elpell14qr  35393  elpell1234qr  35395  jm2.27  35559  rmydioph  35565  expdiophlem1  35572  expdioph  35574  pw2f1ocnv  35588  hbtlem1  35678  hbtlem7  35680  dgraalem  35700  dgraaub  35703  ifpbi2  35799  iunrelexpmin1  35929  binomcxplemnotnn0  36332  2sbc6g  36393  2sbc5g  36394  iotasbc  36397  dropab1  36427  dropab2  36428  disjinfi  37081  mullimc  37258  mullimcf  37265  fourierdlem42  37570  fourierdlem48  37576  fourierdlem50  37578  fourierdlem51  37579  fourierdlem54  37582  fourierdlem86  37614  dfdfat2  38013  pfxeq  38325  2ffzoeq  38403  spthdifv  38412  usgra2pth  38414  edgssv2ALT  38461  edgssv2  38462  isfusgra0  38485  fusgraimpclALT2  38491  mgmhmpropd  38533  ismhm0  38553  isrnghm  38640  rngcsect  38730  rngcinv  38731  rngcsectALTV  38742  rngcinvALTV  38743  ringcsect  38781  ringcinv  38782  ringcsectALTV  38805  ringcinvALTV  38806  lmod1  39035  elbigo2  39114
  Copyright terms: Public domain W3C validator