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

Theorem anbi1d 685
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 22 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32rd 621 1  |-  ( ph  ->  ( ( ps  /\  th )  <->  ( ch  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  anbi1  687  anbi12d  691  bi2anan9  843  pm5.71  902  cador  1381  drsb1  1962  eleq1  2343  rexeqf  2733  reueq1f  2734  rmoeq1f  2735  rabeqf  2781  vtocl2gaf  2850  alexeq  2897  ceqex  2898  sbc2or  2999  sbc5  3015  rexss  3240  psstr  3280  ineq1  3363  difin2  3430  r19.28z  3546  r19.28zv  3549  ssunsn2  3773  preq12bg  3791  opeq1  3796  eluni  3830  disjxun  4021  mpteq12f  4096  axrep1  4132  axrep2  4133  axrep3  4134  zfrepclf  4137  axsep  4140  axsep2  4142  zfauscl  4143  opthg  4246  copsexg  4252  euotd  4267  elopab  4272  pocl  4321  dflim2  4448  uniuni  4527  reusv2lem4  4538  rabxfrd  4555  limuni3  4643  xpeq1  4703  elxpi  4705  vtoclr  4733  opbrop  4767  opelresg  4962  resopab2  4999  elxp4  5160  elxp5  5161  fun11  5315  feq2  5376  f1eq2  5433  f1eq3  5434  foeq2  5448  brprcneu  5518  ssimaexg  5585  dmfco  5593  fndmdif  5629  rexsupp  5650  respreima  5654  opabex3  5769  isoeq5  5820  isoini  5835  isopolem  5842  f1oiso  5848  f1oiso2  5849  oprabid  5882  mpt2eq123  5907  mpt2eq123dva  5909  eloprabga  5934  resoprab  5940  resoprab2  5941  ov  5967  ov3  5984  ov6g  5985  ovg  5986  caoftrn  6112  eloprabi  6186  cnvf1o  6217  frxp  6225  xporderlem  6226  poxp  6227  fnwelem  6230  opiota  6290  riotaeqdv  6305  smoel2  6380  omeu  6583  oeeui  6600  omabs  6645  omopth  6656  qliftel  6741  brecop  6751  eroveu  6753  erov  6755  ecopovtrn  6761  th3qlem2  6765  th3q  6767  ixpsnf1o  6856  dom2lem  6901  xpsnen  6946  xpassen  6956  pw2f1olem  6966  xpf1o  7023  unxpdom  7070  domunfican  7129  preleq  7318  zfinf  7340  cantnfs  7367  tcvalg  7423  r0weon  7640  fseqenlem1  7651  acni2  7673  aceq1  7744  aceq0  7745  dfac2a  7756  dfac12lem2  7770  cardcf  7878  cfeq0  7882  cfsuc  7883  cff1  7884  cfss  7891  isf32lem5  7983  fin1a2lem6  8031  zfac  8086  brdom7disj  8156  brdom6disj  8157  axrepnd  8216  axunndlem1  8217  axinfnd  8228  axacndlem5  8233  axacnd  8234  zfcndrep  8236  zfcndinf  8240  zfcndac  8241  pwfseqlem4a  8283  pwfseqlem4  8284  gruina  8440  grothomex  8451  ordpipq  8566  elnpi  8612  genpass  8633  ltprord  8654  reclem2pr  8672  reclem3pr  8673  recexpr  8675  ltsosr  8716  mulgt0sr  8727  supsr  8734  ltresr  8762  axpre-lttrn  8788  axpre-mulgt0  8790  prime  10092  peano5uzti  10101  uzindOLD  10106  rexuz  10269  ltxr  10457  qbtwnre  10526  xmulneg1  10589  supxr2  10632  ixxval  10664  fzval  10784  nn0opth2  11287  hashbclem  11390  hashf1lem2  11394  abslt  11798  absle  11799  lenegsq  11804  abs2difabs  11818  ello12  11990  elo12  12001  o1lo1  12011  rlimuni  12024  lo1resb  12038  o1resb  12040  2clim  12046  rlimcn2  12064  climcn2  12066  addcn2  12067  mulcn2  12069  o1of2  12086  sumeq1f  12161  fsum2dlem  12233  znnenlem  12490  nndivdvds  12537  divalg2  12604  smupval  12679  gcdval  12687  gcdass  12724  rpexp  12799  pythagtriplem2  12870  pythagtrip  12887  vdwapun  13021  0ram  13067  ramub1lem2  13074  pwsle  13391  imasleval  13443  ismre  13492  ismri  13533  iscatd2  13583  isssc  13697  funcpropd  13774  fullpropd  13794  fthres2b  13804  fthres2c  13805  setcsect  13921  prslem  14065  drsdir  14069  posi  14084  tosso  14142  ipoval  14257  ipolt  14262  odudlatb  14299  dirge  14359  mndpropd  14398  mhmpropd  14421  issubg3  14637  isga  14745  isslw  14919  dprdw  15245  subgdmdprd  15269  drngpropd  15539  issubrg  15545  islmod  15631  lmodlema  15632  lmodprop2d  15687  lsslss  15718  lbspropd  15852  lbsacsbs  15909  aspval2  16086  psrbag  16112  znleval  16508  istopg  16641  basis2  16689  tg2  16703  iscld  16764  neival  16839  isnei  16840  isneip  16842  restlp  16913  iscn  16965  cnpval  16966  iscnp  16967  regsep  17062  nrmsep3  17083  1stcclb  17170  2ndc1stc  17177  2ndcctbss  17181  2ndcdisj  17182  llyi  17200  nllyi  17201  hausmapdom  17226  elkgen  17231  txbas  17262  txcls  17299  txcnpi  17302  ptpjopn  17306  txdis1cn  17329  txtube  17334  txcmplem1  17335  hausdiag  17339  tx1stc  17344  txkgen  17346  xkococnlem  17353  xkococn  17354  elqtop  17388  kqreglem1  17432  elmptrab  17522  isfbas  17524  elflim2  17659  elflim  17666  hauspwpwf1  17682  alexsublem  17738  ghmcnp  17797  divstgplem  17803  tsmssubm  17825  ismet  17888  isxmet  17889  ismet2  17898  imasdsf1olem  17937  blres  17977  elmopn  17988  mopni  18038  neibl  18047  nrmmetd  18097  ngppropd  18153  elcncf  18393  mulc1cncf  18409  elpi1  18543  metcld2  18732  pmltpclem1  18808  ovolval  18833  itg1climres  19069  itg2val  19083  isibl  19120  itgeq1f  19126  itgresr  19133  iblcn  19153  itgfsum  19181  dvreslem  19259  dvfsumlem2  19374  pf1ind  19438  deg1ldg  19478  vieta1  19692  ulm2  19764  sincosq2sgn  19867  sincosq4sgn  19869  efopn  20005  dvdsflsumcom  20428  fsumvma2  20453  logfac2  20456  dchrptlem1  20503  lgsdchrval  20586  pntibndlem3  20741  pntlemi  20753  pntleme  20757  pnt3  20761  drngoi  21074  rngosn3  21093  vci  21104  isvclem  21133  nmoofval  21340  isph  21400  norm3lemt  21731  isch2  21803  cmbr  22163  eigre  22415  eigorth  22418  nmopub  22488  nmfnleub  22505  cvbr  22862  mdbr  22874  dmdbr  22879  chrelat2  22950  mdsymlem2  22984  ifeqeqx  23034  rexunirn  23140  itgeq12dv  23196  funcnvmptOLD  23234  funcnvmpt  23235  gsumpropd2lem  23379  isrrvv  23646  kur14  23747  pconcn  23755  cnpcon  23761  txpcon  23763  cvmscbv  23789  cvmcov  23794  cvmsi  23796  cvmsval  23797  cvmopnlem  23809  cvmlift2lem10  23843  cvmlift3lem2  23851  cvmlift3lem6  23855  cvmlift3lem7  23856  cvmlift3lem9  23858  cvmlift3  23859  eupath2lem2  23902  relexp0  24025  relexpsucr  24026  relexpsucl  24028  relexpcnv  24029  relexpdm  24032  relexprn  24033  relexpadd  24035  relexpindlem  24036  rtrclreclem.trans  24043  rtrclreclem.min  24044  eldm3  24119  dfon2lem6  24144  dfon2lem7  24145  dfon2lem8  24146  dfon2  24148  preduz  24200  poseq  24253  soseq  24254  sltval  24301  nodenselem5  24339  nocvxminlem  24344  brimg  24476  brcgr  24528  brbtwn2  24533  axsegconlem1  24545  axsegcon  24555  axcontlem10  24601  brofs  24628  5segofs  24629  brifs  24666  ifscgr  24667  brcolinear  24682  lineext  24699  brfs  24702  fscgr  24703  linecgr  24704  btwnconn1lem4  24713  btwnconn1lem8  24717  btwnconn1lem11  24720  btwnconn1lem12  24721  segcon2  24728  brsegle  24731  outsideofeq  24753  funray  24763  funline  24765  fvline  24767  linethru  24776  areacirclem6  24930  alexeqd  24962  copsexgb  24966  elo  25041  eloi  25086  islatalg  25183  prodeq1  25306  vecval1b  25451  vecval3b  25452  vri  25492  sallnei  25529  osneisi  25531  qusp  25542  cnfilca  25556  exopcopn  25572  lvsovso  25626  tcnvec  25690  isalg  25721  algi  25727  isded  25736  dedi  25737  iscatOLD  25754  cati  25755  cmpasso  25773  propsrc  25868  vtarsuelt  25895  isrocatset  25957  setiscat  25979  isnword  25986  pgapspf2  26053  isig2a2  26066  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  isibcg  26191  trer  26227  finminlem  26231  ivthALT  26258  locfinnei  26302  comppfsc  26307  filnetlem4  26330  cover2  26358  cover2g  26359  fdc  26455  fdc1  26456  heibor1  26534  bfp  26548  isdrngo1  26587  isriscg  26615  isfldidl2  26694  mrefg2  26782  mzpclval  26803  eldiophb  26836  eldioph2lem1  26839  eldioph3  26845  lzenom  26849  diophin  26852  eldiophss  26854  diophrex  26855  eq0rabdioph  26856  pellexlem3  26916  elpell1qr  26932  elpell14qr  26934  elpell1234qr  26936  jm2.27  27101  rmydioph  27107  expdiophlem1  27114  expdioph  27116  pw2f1ocnv  27130  islbs4  27302  islinds3  27304  hbtlem1  27327  hbtlem7  27329  dgraalem  27350  dgraaub  27353  psgnfval  27423  psgnval  27430  2sbc6g  27615  2sbc5g  27616  iotasbc  27619  dropab1  27650  dropab2  27651  stoweidlem57  27806  dfdfat2  27994  bnj956  28808  bnj1146  28823  bnj18eq1  28959  islshpat  29207  lcvbr  29211  lshpsmreu  29299  ldual1dim  29356  cvrval  29459  cvrnbtwn3  29466  iscvlat2N  29514  ishlat3N  29544  hlrelat5N  29590  3dim0  29646  llnexatN  29710  islpln5  29724  islvol5  29768  pmapjat1  30042  ltrnu  30310  cdleme02N  30411  cdlemg33b  30896  cdlemg33c  30897  dvhb1dimN  31175  dibelval3  31337  dibopelval3  31338  dib1dim  31355  dibglbN  31356  diblsmopel  31361  dicval  31366  dicopelval  31367  dicelval3  31370  dicelval1sta  31377  dihopelvalcpre  31438  dih1dimatlem  31519  dihpN  31526  dihjatcclem4  31611  lpolsetN  31672  mapdpglem3  31865  hdmapglem7a  32120
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 177  df-an 360
  Copyright terms: Public domain W3C validator