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

Theorem anbi2d 696
Description: Deduction adding a left 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
anbi2d  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )

Proof of Theorem anbi2d
StepHypRef Expression
1 bid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21a1d 25 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32d 632 1  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )
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:  anbi2  700  anbi12d  703  bi2anan9  861  2eu6  2363  eleq2  2494  ceqsex2  2999  ceqsex6v  3003  vtocl2gaf  3026  vtocl4ga  3031  ceqsrex2v  3084  moeq3  3125  mob2  3128  eqreu  3140  nelrdva  3157  undif4  3723  r19.27z  3766  r19.27zv  3767  ssunsn2  4020  preq12bg  4039  prel12g  4040  opeq2  4048  ralunsn  4067  intab  4146  disjxun  4278  opabbid  4342  opthg  4555  pocl  4635  isso2i  4660  ordelord  4728  ordtri4  4743  xpeq2  4842  rabxp  4862  vtoclr  4870  opeliunxp  4877  posn  4894  opbrop  4903  elrnmpt1  5075  dfres2  5146  brcodir  5205  poltletr  5221  xp11  5261  fununi  5472  fneq2  5488  fnun  5505  feq3  5532  foeq3  5606  funbrfv  5718  ssimaexg  5745  fvopab3g  5758  fvopab3ig  5759  fvelrn  5827  fvcofneq  5839  fmptco  5863  elunirnALT  5957  isoeq2  5998  isoeq3  5999  isoini  6016  isopolem  6023  f1oiso  6029  f1oiso2  6030  oprabbid  6128  cbvoprab3  6151  mpt2mptx  6170  mpt2fun  6181  elrnmpt2res  6193  ov  6199  ov3  6216  ov6g  6217  ovg  6218  caoftrn  6344  dfwe2  6382  dflim4  6448  tfisi  6458  elxp4  6511  elxp5  6512  f1o2ndf1  6669  frxp  6671  xporderlem  6672  fnwelem  6676  brtpos2  6740  dftpos4  6753  onfununi  6788  recseq  6819  omopth  7085  brecop  7181  eroveu  7183  erovlem  7184  erov  7185  ecopovtrn  7191  th3qlem1  7194  th3qlem2  7195  th3q  7197  elpmg  7216  ixpsnval  7254  ixpsnf1o  7291  domeng  7312  dom2lem  7337  xpcomco  7389  xpassen  7393  xpdom2  7394  omxpenlem  7400  xpf1o  7461  unxpdom  7508  isinf  7514  findcard2  7540  findcard2d  7542  fiint  7576  supeq2  7686  wemapso2lem  7755  inf0  7815  cantnfp1lem3  7876  cantnfp1  7877  scott0  8081  isinffi  8150  isacn  8202  aceq1  8275  aceq0  8276  aceq2  8277  dfac3  8279  dfac5lem1  8281  dfac2  8288  dfac12lem2  8301  kmlem8  8314  kmlem14  8320  infmap2  8375  cfval  8404  cflim3  8419  sornom  8434  infpssrlem4  8463  isf32lem9  8518  domtriomlem  8599  axdc2lem  8605  zfac  8617  ac6num  8636  axrepndlem1  8744  axunndlem1  8747  axregnd  8758  axinfndlem1  8759  axacndlem4  8764  axacndlem5  8765  zfcndac  8773  fpwwe2lem5  8788  pwfseqlem4a  8815  pwfseqlem4  8816  alephgch  8828  wunex2  8892  tskord  8934  nqereu  9085  ordpipq  9098  prcdnq  9149  prnmax  9151  genpnnp  9161  distrlem5pr  9183  ltprord  9186  ltexprlem3  9194  ltexprlem4  9195  ltexpri  9199  prlem936  9203  reclem2pr  9204  ltsosr  9248  mulgt0sr  9259  ltresr  9294  axpre-lttrn  9320  axpre-mulgt0  9322  eqlelt  9449  lesub0  9843  wloglei  9859  mulle0b  10187  sup3  10274  infm3  10276  prime  10709  fzind  10727  uzwo  10904  uzwoOLD  10905  zbtwnre  10938  xltnegi  11173  xmulneg1  11219  ixxval  11295  fzval  11425  elfzm11  11511  elfzo  11538  seqof2  11847  nn0opth2  12033  facwordi  12048  hashnn0n0nn  12136  brfi1uzind  12202  wrdeqswrdlsw  12326  2swrd1eqwrdeq  12331  wrd2ind  12355  2swrd2eqwrdeq  12536  shftfval  12542  shftfib  12544  shftfn  12545  2shfti  12552  abs1m  12806  cau3lem  12825  caubnd2  12828  clim  12955  rlim  12956  clim2  12965  climi  12971  o1lo1  12998  rlimcn2  13051  climcn2  13053  addcn2  13054  subcn2  13055  mulcn2  13056  o1of2  13073  isercoll  13128  caurcvg2  13138  sumeq2w  13152  sumeq2ii  13153  summo  13177  fsum  13180  sinbnd  13446  cosbnd  13447  divalgb  13590  ndvdssub  13593  smupp1  13658  smueqlem  13668  gcdval  13674  gcdcllem2  13678  gcdneg  13692  gcdass  13711  algcvgblem  13734  prmind2  13756  qredeq  13774  euclemma  13776  qnumval  13797  qdenval  13798  eulerthlem2  13839  pceu  13895  pczpre  13896  pcdiv  13901  prmpwdvds  13947  prmreclem5  13963  vdwapun  14017  ramub2  14057  rami  14058  ramcl  14072  ismred2  14523  isacs  14571  iscatd2  14601  catpropd  14630  oppccatid  14640  isinv  14680  isssc  14715  funcres2b  14789  funcpropd  14792  fucinv  14865  yoniso  15077  prslem  15083  drsdir  15087  drsdirfi  15090  posi  15102  isposd  15107  pltval  15112  plttr  15122  isipodrs  15313  ipodrsima  15317  dirge  15389  mndlem1  15401  mrcmndind  15475  gsumpropd  15485  gsumress  15486  divsgrp2  15652  resscntz  15828  psgnunilem3  15981  psgneu  15991  psgnvali  15993  psgnvalii  15994  isslw  16086  subgslw  16094  iscmnd  16268  gsumval3eu  16360  gsumval3OLD  16361  gsumval3lem2  16363  dmdprd  16453  subgdmdprd  16504  dprd2d2  16516  pgpfac1  16554  pgpfaclem2  16556  pgpfaclem3  16557  pgpfac  16558  ablfaclem1  16559  divsrng2  16646  dvdsrval  16670  crngunit  16687  dfrhm2  16741  isdrngd  16780  abvpropd  16850  islmod  16875  lssacs  16969  lsspropd  17019  islmhm  17029  lbspropd  17101  ixpsnbasval  17211  fiidomfld  17301  ltbval  17484  opsrval  17487  psgndiflemA  17872  pjfval2  17975  frlmup1  18067  mdetralt  18255  mdetralt2  18256  mdetunilem1  18259  mdetunilem2  18260  mdetunilem9  18267  gsummatr01  18306  eltopspOLD  18364  istpsOLD  18366  basis2  18397  eltg2  18404  isclo  18532  isnei  18548  isneip  18550  neiptopnei  18577  restbas  18603  restcld  18617  neitr  18625  iscnp  18682  iscnp3  18689  tgcn  18697  cnpimaex  18701  lmbrf  18705  cncnp  18725  cnprest2  18735  isreg  18777  regsep  18779  isnrm  18780  ist1-2  18792  nrmsep3  18800  isnrm2  18803  hauscmplem  18850  dfcon2  18864  is1stc  18886  1stcclb  18889  1stcfb  18890  is2ndc  18891  2ndc1stc  18896  1stcrest  18898  2ndcsep  18904  1stccnp  18907  islly  18913  llyeq  18915  llyi  18919  hausllycmp  18939  lly1stc  18941  txbas  18981  ptpjpre1  18985  elpt  18986  txcnpi  19022  ptpjopn  19026  ptcldmpt  19028  ptclsg  19029  txcnp  19034  ptcnp  19036  hausdiag  19059  tx1stc  19064  xkoinjcn  19101  imasnopn  19104  imasncld  19105  imasncls  19106  fbfinnfr  19255  snfil  19278  uffix2  19338  elfm  19361  elfm2  19362  fmco  19375  hauspwpwf1  19401  flfnei  19405  isflf  19407  lmflf  19419  fclscf  19439  isfcf  19448  alexsublem  19457  cnextcn  19480  cnextfres  19481  eltsms  19544  tsmsresOLD  19558  tsmsres  19559  tsmsf1o  19560  ustuqtop4  19660  ispsmet  19721  ismet  19739  isxmet  19740  ismet2  19749  imasdsf1olem  19789  blres  19847  met2ndc  19939  metcnp3  19956  nrmmetd  20008  pi1grplem  20462  lmmbr2  20611  lmmbrf  20614  iscau2  20629  iscau4  20631  caucfil  20635  lmclim  20654  cfilucfil3OLD  20670  cfilucfil3  20671  bcthlem1  20676  bcth  20681  ishl2  20723  pmltpclem1  20773  elovolm  20799  ovolgelb  20804  ovolicc  20847  mbfaddlem  20979  i1fres  21024  mbfi1fseqlem4  21037  itg2l  21048  itg2leub  21053  itg2seq  21061  isibl  21084  iblitg  21087  dfitg  21088  itgeq2  21096  itgvallem  21103  iblcnlem1  21106  iblrelem  21109  iblpos  21111  ellimc3  21195  limciun  21210  limcun  21211  dvmptfsum  21288  dveflem  21292  lhop1lem  21326  dvfsumlem2  21340  dvfsumlem4  21342  mpfind  21395  pf1ind  21405  mdegleb  21419  elply2  21548  plypf1  21564  coeval  21575  plydivlem4  21646  sincosq3sgn  21846  vmasum  22439  lgsqrlem1  22564  lgsquadlem1  22577  2sqlem8  22595  2sqlem9  22596  2sqlem11  22598  dchrisumlema  22621  dchrisumlem2  22623  pntibndlem3  22725  pntibnd  22726  pntleme  22741  pntlemp  22743  axtgsegcon  22809  axtg5seg  22810  axtgpasch  22812  iscgrg  22845  legov  22891  mirreu3  22923  brcgr  22968  brbtwn2  22973  colinearalg  22978  ax5seg  23006  axcontlem5  23036  axcontlem10  23041  usgraedg4  23127  cusgrafilem2  23210  cusgrafi  23212  uvtx01vtx  23222  usgrnloop  23284  spthonepeq  23308  usgrcyclnl2  23349  4cycl4v4e  23374  4cycl4dv4e  23376  iseupa  23408  eupath2lem3  23422  isgrpo  23505  isgrp2d  23544  isgrpda  23606  ismndo  23652  drngoi  23716  vci  23748  isvclem  23777  nmoofval  23984  nmooval  23985  nmosetn0  23987  nmoolb  23993  nmoubi  23994  nmoo0  24013  nmlno0lem  24015  isphg  24039  norm3lemt  24376  chlimi  24459  ocsh  24508  cmbr  24809  chscllem2  24863  spansncv  24878  eigorth  25064  nmopval  25082  nmopsetn0  25091  nmfnval  25102  nmfnsetn0  25104  nmoplb  25133  nmfnlb  25150  nmopnegi  25191  nmop0  25212  nmfn0  25213  nmlnop0iALT  25221  nmopun  25240  nmcexi  25252  branmfn  25331  leopmuli  25359  pjnmopi  25374  cvbr  25508  mdbr  25520  dmdbr  25525  atom1d  25579  chrelat2  25596  atcvati  25612  atord  25614  atcvat2  25615  chirredlem4  25619  mdsymlem5  25633  disjunsn  25759  fmptcof2  25802  ofpreima  25807  funcnv4mpt  25812  mpt2mptxf  25818  2ndpreima  25825  f1od2  25847  xeqlelt  25888  ishashinf  25907  ressprs  25938  isomnd  25987  archiabllem2a  26034  archiabl  26038  isslmd  26066  gsumle  26097  gsumvsca1  26103  gsumvsca2  26104  esumcvg  26388  sitgval  26565  eulerpartlemgvv  26606  eulerpartlemn  26611  eulerpart  26612  brafs  26843  lgamgulmlem2  26863  erdszelem3  26928  erdsze  26937  pconcn  26960  cnpcon  26966  txpcon  26968  conpcon  26971  cvmscbv  26994  iscvm  26995  cvmsi  27001  cvmsval  27002  relexp0  27177  relexpsucr  27178  relexpsucl  27180  relexpadd  27186  relexpindlem  27187  prodfdiv  27257  ntrivcvgn0  27259  ntrivcvgmullem  27262  prodeq1f  27267  prodeq2w  27271  prodeq2ii  27272  prodmo  27295  zprod  27296  fprod  27300  fprodntriv  27301  elima4  27436  dfrdg2  27455  dfrdg3  27456  elpred  27484  trpredrec  27548  poseq  27560  soseq  27561  sltval  27634  nocvxminlem  27677  nofulllem1  27689  elfuns  27792  brimg  27814  brsuccf  27818  dfrdg4  27827  tfrqfree  27828  brofs  27882  funtransport  27908  fvtransport  27909  brifs  27920  lineext  27953  brfs  27956  btwnconn1lem11  27974  btwnconn1lem14  27977  brsegle  27985  segletr  27991  segleantisym  27992  seglelin  27993  funray  28017  fvray  28018  funline  28019  fvline  28021  ellines  28029  linethru  28030  ptrest  28266  mblfinlem3  28271  mblfinlem4  28272  ismblfin  28273  mbfresfi  28279  itg2addnclem  28284  itg2addnclem3  28286  itg2addnc  28287  ftc1anclem7  28314  ftc1anc  28316  areacirclem5  28329  trer  28352  opnrebl2  28357  nn0prpwlem  28358  isfne4  28382  isfne2  28384  isfne3  28385  islocfin  28409  unirep  28447  fnopabeqd  28454  fdc  28482  fdc1  28483  istotbnd  28509  heibor1lem  28549  heibor  28561  isriscg  28631  iscringd  28640  isidlc  28656  prtlem16  28856  prtlem15  28862  ismrcd1  28876  ismrcd2  28877  mzpcompact2lem  28930  eldioph  28938  eldioph2  28942  eldioph2b  28943  eldioph3  28946  diophin  28953  diophun  28954  diophrex  28956  rexrabdioph  28974  fphpd  28997  fphpdo  28998  pellexlem3  29014  monotuz  29124  monotoddzzfi  29125  monotoddzz  29126  oddcomabszz  29127  jm2.27  29199  rmydioph  29205  expdiophlem1  29212  expdiophlem2  29213  aomclem6  29254  aomclem8  29256  islssfg  29265  islssfg2  29266  hbtlem2  29322  hbtlem4  29324  hbtlem5  29326  hbtlem6  29327  dgraaval  29343  flcidc  29373  2sbc6g  29511  2sbc5g  29512  iotasbc2  29516  pm14.122a  29518  pm14.123a  29521  fmul01  29603  fmuldfeqlem1  29605  fmuldfeq  29606  fmul01lt1lem1  29607  fmul01lt1lem2  29608  climmulf  29620  climexp  29621  climsuse  29624  climrecf  29625  climinff  29627  stoweidlem3  29641  stoweidlem4  29642  stoweidlem7  29645  stoweidlem15  29653  stoweidlem16  29654  stoweidlem17  29655  stoweidlem19  29657  stoweidlem20  29658  stoweidlem22  29660  stoweidlem23  29661  stoweidlem27  29665  stoweidlem30  29668  stoweidlem32  29670  stoweidlem34  29672  stoweidlem42  29680  stoweidlem43  29681  stoweidlem48  29686  stoweidlem51  29689  stoweidlem59  29697  stoweidlem60  29698  2reu4a  29856  f12dfv  29989  f13dfv  29990  oprabv  30000  usgra2wlkspthlem1  30139  wwlk  30158  wlklniswwlkn2  30177  el2wlkonot  30231  el2spthonot  30232  el2spthonot0  30233  usg2spthonot  30250  usg2spthonot0  30251  usg2spthonot1  30252  clwlkisclwwlklem0  30293  clwlkisclwwlk  30294  erclwwlktr0  30322  eleclclwwlkn  30350  usghashecclwwlk  30352  isrusgra  30387  rusgranumwlkl1  30402  1vwmgra  30438  3vfriswmgra  30440  3cyclfrgrarn1  30447  4cycl2vnunb  30452  vdn1frgrav2  30461  vdgn1frgrav2  30462  frgrancvvdeqlemB  30474  usg2spot2nb  30501  usgreg2spot  30503  2spotmdisj  30504  usgreghash2spot  30505  extwwlkfab  30526  numclwwlk2lem1  30538  numclwwlk5  30548  opeliun2xp  30562  mpt2mptx2  30566  lcoval  30652  lco0  30667  islinindfis  30689  snlindsntor  30711  mnd1  30727  bnj976  31470  bnj852  31613  bnj1014  31652  bnj1015  31653  bnj1118  31674  bnj1123  31676  bnj1148  31686  bnj1171  31690  bnj1373  31720  bnj1489  31746  bj-finsumval0  32156  lsmsat  32223  lsmsatcv  32225  islshpat  32232  lcvfbr  32235  lcvbr  32236  lsatcv0  32246  islshpkrN  32335  cvrval  32484  cvrval2  32489  cvrnbtwn2  32490  cvlexch1  32543  hlsuprexch  32595  cvrval5  32629  cvrat  32636  cvrat42  32658  3dim0  32671  3dim2  32682  islpln3  32747  islpln5  32749  islvol3  32790  islvol5  32793  4atlem11  32823  lineset  32952  isline  32953  ispsubsp2  32960  isline2  32988  isline3  32990  elpaddat  33018  elpadd2at  33020  dalawlem15  33099  pclfinclN  33164  4atex  33290  4atex2  33291  4atex3  33295  ltrnu  33335  cdleme0nex  33504  cdleme31so  33593  cdleme31fv  33604  cdleme31fv2  33607  cdlemefrs29pre00  33609  cdlemefrs29cpre1  33612  cdlemftr3  33779  cdlemb3  33820  cdlemg6d  33835  cdlemg33b  33921  cdlemg33c  33922  cdlemg33e  33924  cdlemk42  34155  dvhopellsm  34332  dibelval3  34362  diblsmopel  34386  diclspsn  34409  dihval  34447  dihopelvalcpre  34463  dih1dimatlem  34544  dihglb2  34557  dochkrshp3  34603  dihjatcclem4  34636  dihjat1lem  34643  mapdval  34843  mapdpglem30  34917
  Copyright terms: Public domain W3C validator