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  871  pm5.71  934  cador  1442  drsb1  2091  eleq1d  2536  eleq1OLD  2541  rexeqf  3055  reueq1f  3056  rmoeq1f  3057  rabeqf  3106  vtocl2gaf  3178  vtocl4ga  3183  alexeqg  3232  alexeq  3233  elrabi  3258  reu2eqd  3300  sbc2or  3340  sbc5  3356  rexss  3567  psstr  3608  ineq1  3693  difin2  3760  r19.28z  3920  r19.28zv  3923  rabsnifsb  4095  ssunsn2  4186  preq12bg  4205  prel12g  4206  opeq1  4213  eluni  4248  csbuni  4273  disjxun  4445  mpteq12f  4523  axrep1  4559  axrep2  4560  axrep3  4561  zfrepclf  4564  axsep  4567  axsep2  4569  zfauscl  4570  reusv2lem4  4651  rabxfrd  4668  opthg  4722  otthg  4730  copsexg  4732  copsexgOLD  4733  euotd  4748  elopab  4755  pocl  4807  dflim2  4934  xpeq1  5013  elxpi  5015  vtoclr  5044  opbrop  5079  opelresg  5281  resopab2  5322  fun11  5653  feq2  5714  f1eq2  5777  f1eq3  5778  foeq2  5792  brprcneu  5859  ssimaexg  5933  dmfco  5941  fndmdif  5985  rexsuppOLD  6006  respreima  6010  isoeq5  6207  isoini  6222  isopolem  6229  f1oiso  6235  f1oiso2  6236  riotaeqdv  6246  oprabid  6308  oprabv  6329  mpt2eq123  6340  mpt2eq123dva  6342  eloprabga  6373  resoprab  6382  resoprab2  6383  elrnmpt2res  6400  ov  6406  ov3  6423  ov6g  6424  ovg  6425  caoftrn  6559  uniuni  6593  limuni3  6671  elxp4  6728  elxp5  6729  opabex3d  6762  opabex3  6763  opiota  6843  eloprabi  6846  cnvf1o  6882  frxp  6893  xporderlem  6894  poxp  6895  fnwelem  6898  suppimacnv  6912  rexsupp  6918  mpt2curryd  6998  smoel2  7034  omeu  7234  oeeui  7251  omabs  7296  omopth  7307  qliftel  7394  brecop  7404  eroveu  7406  erov  7408  ecopovtrn  7414  ixpsnf1o  7509  dom2lem  7555  xpsnen  7601  xpassen  7611  pw2f1olem  7621  xpf1o  7679  unxpdom  7727  domunfican  7793  preleq  8034  zfinf  8056  cantnfs  8085  cantnfsOLD  8115  tcvalg  8169  r0weon  8390  fseqenlem1  8405  acni2  8427  aceq1  8498  aceq0  8499  dfac2a  8510  dfac12lem2  8524  cardcf  8632  cfeq0  8636  cfsuc  8637  cff1  8638  cfss  8645  isf32lem5  8737  fin1a2lem6  8785  zfac  8840  brdom7disj  8909  brdom6disj  8910  axrepnd  8969  axunndlem1  8970  axinfnd  8984  axacndlem5  8989  axacnd  8990  zfcndrep  8992  zfcndinf  8996  zfcndac  8997  pwfseqlem4a  9039  pwfseqlem4  9040  gruina  9196  grothomex  9207  ordpipq  9320  elnpi  9366  genpass  9387  ltprord  9408  reclem2pr  9426  reclem3pr  9427  recexpr  9429  addsrmo  9450  mulsrmo  9451  addsrpr  9452  mulsrpr  9453  ltsosr  9471  mulgt0sr  9482  supsr  9489  ltresr  9517  axpre-lttrn  9543  axpre-mulgt0  9545  prime  10941  peano5uzti  10950  uzindOLD  10955  rexuz  11131  ltxr  11324  qbtwnre  11398  xmulneg1  11461  supxr2  11505  ixxval  11537  fzval  11674  nn0opth2  12320  hashbclem  12467  hashf1lem2  12471  eqwrd  12547  swrdeq  12634  wrd2ind  12666  cshwcsh2id  12759  abslt  13110  absle  13111  lenegsq  13116  abs2difabs  13130  ello12  13302  elo12  13313  o1lo1  13323  rlimuni  13336  lo1resb  13350  o1resb  13352  2clim  13358  rlimcn2  13376  climcn2  13378  addcn2  13379  mulcn2  13381  o1of2  13398  sumeq1  13474  fsum2dlem  13548  modfsummod  13571  znnenlem  13806  nndivdvds  13853  divalg2  13922  smupval  13997  gcdval  14005  gcdass  14042  rpexp  14120  pythagtriplem2  14200  pythagtrip  14217  vdwapun  14351  0ram  14397  ramub1lem2  14404  pwsle  14747  imasleval  14796  ismre  14845  ismri  14886  iscatd2  14936  isssc  15050  funcpropd  15127  fullpropd  15147  fthres2b  15157  fthres2c  15158  setcsect  15274  prslem  15418  drsdir  15422  posi  15437  tosso  15523  ipoval  15641  ipolt  15646  odudlatb  15683  dirge  15724  mndpropd  15764  mhmpropd  15792  mrcmndind  15816  gsumpropd2lem  15827  issubg3  16024  isga  16134  symgfixelq  16263  psgnfval  16331  psgnval  16338  isslw  16434  dprdw  16846  dprdwOLD  16852  subgdmdprd  16883  drngpropd  17223  issubrg  17229  islmod  17316  lmodlema  17317  lmodprop2d  17372  lsslss  17407  lbspropd  17545  lbsacsbs  17602  aspval2  17795  psrbag  17812  pf1ind  18190  znleval  18388  islbs4  18662  islinds3  18664  mdetunilem4  18912  mdetunilem9  18917  istopg  19199  basis2  19247  tg2  19261  iscld  19322  neival  19397  isnei  19398  isneip  19400  neiptoptop  19426  neiptopnei  19427  neitr  19475  restlp  19478  iscn  19530  cnpval  19531  iscnp  19532  regsep  19629  nrmsep3  19650  1stcclb  19739  2ndc1stc  19746  2ndcctbss  19750  2ndcdisj  19751  llyi  19769  nllyi  19770  hausmapdom  19795  elkgen  19800  txbas  19831  txcls  19868  txcnpi  19872  ptpjopn  19876  txdis1cn  19899  txtube  19904  txcmplem1  19905  hausdiag  19909  tx1stc  19914  txkgen  19916  xkococnlem  19923  xkococn  19924  elqtop  19961  kqreglem1  20005  elmptrab  20091  isfbas  20093  elflim2  20228  elflim  20235  hauspwpwf1  20251  alexsublem  20307  ghmcnp  20376  divstgplem  20382  tsmssubm  20407  elutop  20499  ustuqtop4  20510  isucn  20544  iscfilu  20554  ispsmet  20571  ismet  20589  isxmet  20590  ismet2  20599  imasdsf1olem  20639  blres  20697  elmopn  20708  mopni  20758  neibl  20767  nrmmetd  20858  ngppropd  20914  elcncf  21156  mulc1cncf  21172  elpi1  21308  metcld2  21508  pmltpclem1  21623  ovolval  21648  itg1climres  21884  itg2val  21898  isibl  21935  itgeq1f  21941  itgresr  21948  iblcn  21968  itgfsum  21996  dvreslem  22076  dvfsumlem2  22191  deg1ldg  22255  vieta1  22470  ulm2  22542  sincosq2sgn  22653  sincosq4sgn  22655  efopn  22795  dvdsflsumcom  23220  fsumvma2  23245  logfac2  23248  dchrptlem1  23295  lgsdchrval  23378  pntibndlem3  23533  pntlemi  23545  pntleme  23549  pnt3  23553  istrkg2d  23612  istrkgld  23613  istrkg2ld  23614  axtgsegcon  23617  axtg5seg  23618  axtgpasch  23620  axtgupdim2  23625  legov  23727  brcgr  23907  brbtwn2  23912  axsegconlem1  23924  axsegcon  23934  axcontlem10  23980  usgra2edg  24086  trls  24242  istrl2  24244  trlon  24246  is2wlk  24271  spths  24273  0spth  24277  pthon  24281  spthon  24288  isspthonpth  24290  usgra2wlkspthlem1  24323  0crct  24330  0cycl  24331  usgrcyclnl2  24345  wwlknprop  24390  vfwlkniswwlkn  24410  wwlknext  24428  wwlknfi  24442  clwlk  24457  isclwlk  24460  clwlkcompim  24468  clwwlkn2  24479  clwwlknimp  24480  clwwlkel  24497  clwwlkf  24498  clwwlkext2edg  24506  wwlkext2clwwlk  24507  wwlksubclwwlk  24508  erclwwlknsym  24530  erclwwlkntr  24531  clwlkfoclwwlk  24549  el2wlkonotot0  24576  2spontn0vne  24591  rusgranumwlkl1  24651  rusgranumwlklem3  24655  rusgranumwlkb0  24657  rusgra0edg  24659  eupath2lem2  24682  3cyclfrgrarn1  24716  4cycl2vnunb  24721  frg2wot1  24762  usg2spot2nb  24770  extwwlkfablem2  24783  numclwwlkovfel2  24788  numclwwlkovf2  24789  numclwwlkovf2ex  24791  numclwwlkovgel  24793  numclwwlkovgelim  24794  numclwlk2lem2f  24808  numclwlk2lem2f1o  24810  numclwwlk5  24817  drngoi  25113  rngosn3  25132  vci  25145  isvclem  25174  nmoofval  25381  isph  25441  norm3lemt  25773  isch2  25845  cmbr  26206  eigre  26458  eigorth  26461  nmopub  26531  nmfnleub  26548  cvbr  26905  mdbr  26917  dmdbr  26922  chrelat2  26993  mdsymlem2  27027  rexunirn  27094  ifeqeqx  27121  funcnvmptOLD  27209  funcnvmpt  27210  1stpreima  27224  fpwrelmapffslem  27255  isomnd  27381  archirng  27422  isslmd  27435  slmdlema  27436  dya2iocuni  27922  omsfval  27933  itgeq12dv  27936  isrrvv  28050  brafs  28220  kur14  28328  pconcn  28337  cnpcon  28343  txpcon  28345  cvmscbv  28371  cvmcov  28376  cvmsi  28378  cvmsval  28379  cvmopnlem  28391  cvmlift2lem10  28425  cvmlift3lem2  28433  cvmlift3lem6  28437  cvmlift3lem7  28438  cvmlift3lem9  28440  cvmlift3  28441  relexp0  28555  relexpsucr  28556  relexpsucl  28558  relexpcnv  28559  relexpdm  28561  relexprn  28562  relexpadd  28564  relexpindlem  28565  rtrclreclem.trans  28572  rtrclreclem.min  28573  prodeq1f  28645  fprod2dlem  28715  eldm3  28796  opelco3  28813  dfon2lem6  28825  dfon2lem7  28826  dfon2lem8  28827  dfon2  28829  preduz  28885  poseq  28938  soseq  28939  sltval  29012  nodenselem5  29050  nocvxminlem  29055  elfuns  29170  brofs  29260  5segofs  29261  brifs  29298  ifscgr  29299  brcolinear  29314  lineext  29331  brfs  29334  fscgr  29335  linecgr  29336  btwnconn1lem4  29345  btwnconn1lem8  29349  btwnconn1lem11  29352  btwnconn1lem12  29353  segcon2  29360  brsegle  29363  outsideofeq  29385  funray  29395  funline  29397  fvline  29399  linethru  29408  wl-ax11-lem8  29637  ptrest  29653  heicant  29654  mblfinlem3  29658  mblfinlem4  29659  mbfresfi  29666  itg2addnclem3  29673  itg2addnc  29674  itg2gt0cn  29675  areacirclem5  29716  trer  29739  finminlem  29741  ivthALT  29758  locfinnei  29802  comppfsc  29807  filnetlem4  29830  cover2  29835  cover2g  29836  fdc  29869  fdc1  29870  heibor1  29937  bfp  29951  isdrngo1  29990  isriscg  30018  isfldidl2  30097  mrefg2  30271  mzpclval  30289  eldiophb  30322  eldioph2lem1  30325  eldioph3  30331  lzenom  30335  diophin  30338  eldiophss  30340  diophrex  30341  eq0rabdioph  30342  pellexlem3  30399  elpell1qr  30415  elpell14qr  30417  elpell1234qr  30419  jm2.27  30582  rmydioph  30588  expdiophlem1  30595  expdioph  30597  pw2f1ocnv  30611  hbtlem1  30704  hbtlem7  30706  dgraalem  30727  dgraaub  30730  lcmval  30826  lcmass  30846  2sbc6g  30928  2sbc5g  30929  iotasbc  30932  dropab1  30962  dropab2  30963  mullimc  31186  mullimcf  31193  fourierdlem42  31477  fourierdlem48  31483  fourierdlem50  31485  fourierdlem51  31486  fourierdlem54  31489  fourierdlem86  31521  dfdfat2  31711  2ffzoeq  31836  spthdifv  31847  usgra2pth  31849  edgssv2ALT  31896  edgssv2  31897  isfusgra0  31920  fusgraimpclALT2  31926  lmod1  32192  bnj956  32932  bnj1146  32947  bnj18eq1  33082  bj-axrep1  33473  bj-axrep2  33474  bj-axrep3  33475  bj-axsep  33478  bj-eleq1w  33521  bj-rabeqd  33587  bj-axsep2  33592  islshpat  33832  lcvbr  33836  lshpsmreu  33924  ldual1dim  33981  cvrval  34084  cvrnbtwn3  34091  iscvlat2N  34139  ishlat3N  34169  hlrelat5N  34215  3dim0  34271  llnexatN  34335  islpln5  34349  islvol5  34393  pmapjat1  34667  ltrnu  34935  cdleme02N  35036  cdlemg33b  35521  cdlemg33c  35522  dvhb1dimN  35800  dibelval3  35962  dibopelval3  35963  dib1dim  35980  dibglbN  35981  diblsmopel  35986  dicval  35991  dicopelval  35992  dicelval3  35995  dicelval1sta  36002  dihopelvalcpre  36063  dih1dimatlem  36144  dihpN  36151  dihjatcclem4  36236  lpolsetN  36297  mapdpglem3  36490  hdmapglem7a  36745
  Copyright terms: Public domain W3C validator