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

Theorem anbi2d 684
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 22 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32d 620 1  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  anbi2  688  anbi12d  691  bi2anan9  843  2eu6  2228  eleq2  2344  ceqsex2  2824  ceqsex6v  2828  vtocl2gaf  2850  ceqsrex2v  2903  moeq3  2942  mob2  2945  eqreu  2957  undif4  3511  r19.27z  3552  r19.27zv  3553  ssunsn2  3773  preq12bg  3791  opeq2  3797  ralunsn  3815  intab  3892  disjxun  4021  opabbid  4081  opthg  4246  pocl  4321  isso2i  4346  ordelord  4414  ordtri4  4429  dfwe2  4573  dflim4  4639  tfisi  4649  xpeq2  4704  rabxp  4725  vtoclr  4733  opeliunxp  4740  posn  4758  opbrop  4767  elrnmpt1  4928  dfres2  5002  brcodir  5062  poltletr  5078  xp11  5111  elxp4  5160  elxp5  5161  fununi  5316  fneq2  5334  fnun  5350  feq3  5377  foeq3  5449  funbrfv  5561  ssimaexg  5585  fvopab3g  5598  fvopab3ig  5599  fvelrn  5661  fmptco  5691  elunirnALT  5779  isoeq2  5817  isoeq3  5818  isoini  5835  isopolem  5842  f1oiso  5848  f1oiso2  5849  oprabbid  5901  cbvoprab3  5922  mpt2mptx  5938  mpt2fun  5946  ov  5967  ov3  5984  ov6g  5985  ovg  5986  caoftrn  6112  frxp  6225  xporderlem  6226  fnwelem  6230  brtpos2  6240  dftpos4  6253  riotabidv  6306  onfununi  6358  recseq  6389  tfrlem1  6391  omopth  6656  brecop  6751  eroveu  6753  erovlem  6754  erov  6755  ecopovtrn  6761  th3qlem1  6764  th3qlem2  6765  th3q  6767  elpmg  6786  ixpsnf1o  6856  domeng  6876  dom2lem  6901  xpcomco  6952  xpassen  6956  xpdom2  6957  omxpenlem  6963  xpf1o  7023  unxpdom  7070  isinf  7076  findcard2  7098  fiint  7133  supeq2  7201  inf0  7322  scott0  7556  isinffi  7625  isacn  7671  aceq1  7744  aceq0  7745  aceq2  7746  dfac3  7748  dfac5lem1  7750  dfac2  7757  dfac12lem2  7770  kmlem8  7783  kmlem14  7789  infmap2  7844  cfval  7873  cflim3  7888  sornom  7903  infpssrlem4  7932  isf32lem9  7987  domtriomlem  8068  axdc2lem  8074  zfac  8086  ac6num  8106  axrepndlem1  8214  axunndlem1  8217  axregnd  8226  axinfndlem1  8227  axacndlem4  8232  axacndlem5  8233  zfcndac  8241  fpwwe2lem5  8256  pwfseqlem4a  8283  pwfseqlem4  8284  alephgch  8300  wunex2  8360  tskord  8402  nqereu  8553  ordpipq  8566  prcdnq  8617  prnmax  8619  genpnnp  8629  distrlem5pr  8651  ltprord  8654  ltexprlem3  8662  ltexprlem4  8663  ltexpri  8667  prlem936  8671  reclem2pr  8672  ltsosr  8716  mulgt0sr  8727  ltresr  8762  axpre-lttrn  8788  axpre-mulgt0  8790  eqlelt  8909  lesub0  9290  wloglei  9305  sup3  9711  infm3  9713  prime  10092  fzind  10110  uzwo  10281  uzwoOLD  10282  zbtwnre  10314  xltnegi  10543  xmulneg1  10589  ixxval  10664  fzval  10784  elfzm11  10853  elfzo  10877  nn0opth2  11287  facwordi  11302  shftfval  11565  shftfib  11567  shftfn  11568  2shfti  11575  abs1m  11819  cau3lem  11838  caubnd2  11841  clim  11968  rlim  11969  clim2  11978  climi  11984  o1lo1  12011  rlimcn2  12064  climcn2  12066  addcn2  12067  subcn2  12068  mulcn2  12069  o1of2  12086  isercoll  12141  caurcvg2  12150  sumeq2w  12165  sumeq2ii  12166  cbvsum  12168  summo  12190  fsum  12193  sinbnd  12460  cosbnd  12461  divalgb  12603  ndvdssub  12606  smupp1  12671  smueqlem  12681  gcdval  12687  gcdcllem2  12691  gcdneg  12705  gcdass  12724  algcvgblem  12747  prmind2  12769  qredeq  12785  euclemma  12787  qnumval  12808  qdenval  12809  eulerthlem2  12850  pceu  12899  pczpre  12900  pcdiv  12905  prmpwdvds  12951  prmreclem5  12967  vdwapun  13021  ramub2  13061  rami  13062  ramcl  13076  ismred2  13505  isacs  13553  iscatd2  13583  catpropd  13612  oppccatid  13622  isinv  13662  isssc  13697  funcres2b  13771  funcpropd  13774  fucinv  13847  yoniso  14059  prslem  14065  drsdir  14069  drsdirfi  14072  posi  14084  isposd  14089  pltval  14094  plttr  14104  isipodrs  14264  ipodrsima  14268  spwval  14334  dirge  14359  mndlem1  14371  gsumpropd  14453  gsumress  14454  divsgrp2  14613  resscntz  14807  isslw  14919  subgslw  14927  iscmnd  15101  gsumval3eu  15190  gsumval3  15191  dmdprd  15236  subgdmdprd  15269  dprd2d2  15279  pgpfac1  15315  pgpfaclem2  15317  pgpfaclem3  15318  pgpfac  15319  ablfaclem1  15320  divsrng2  15403  dvdsrval  15427  crngunit  15444  dfrhm2  15498  isdrngd  15537  abvpropd  15607  islmod  15631  lssacs  15724  lsspropd  15774  islmhm  15784  lbspropd  15852  fiidomfld  16049  ltbval  16213  opsrval  16216  pjfval2  16609  eltopspOLD  16656  istpsOLD  16658  basis2  16689  eltg2  16696  isclo  16824  isnei  16840  isneip  16842  restbas  16889  restcld  16903  iscnp  16967  iscnp3  16974  tgcn  16982  cnpimaex  16986  lmbrf  16990  cncnp  17009  cnprest2  17018  isreg  17060  regsep  17062  isnrm  17063  ist1-2  17075  nrmsep3  17083  isnrm2  17086  hauscmplem  17133  dfcon2  17145  is1stc  17167  1stcclb  17170  1stcfb  17171  is2ndc  17172  2ndc1stc  17177  1stcrest  17179  2ndcsep  17185  1stccnp  17188  islly  17194  llyeq  17196  llyi  17200  hausllycmp  17220  lly1stc  17222  txbas  17262  ptpjpre1  17266  elpt  17267  txcnpi  17302  ptpjopn  17306  ptcldmpt  17308  ptclsg  17309  txcnp  17314  ptcnp  17316  hausdiag  17339  tx1stc  17344  xkoinjcn  17381  fbfinnfr  17536  snfil  17559  uffix2  17619  elfm  17642  elfm2  17643  fmco  17656  hauspwpwf1  17682  flfnei  17686  isflf  17688  lmflf  17700  fclscf  17720  isfcf  17729  alexsublem  17738  eltsms  17815  tsmsres  17826  tsmsf1o  17827  ismet  17888  isxmet  17889  ismet2  17898  imasdsf1olem  17937  blres  17977  met2ndc  18069  metcnp3  18086  nrmmetd  18097  pi1grplem  18547  lmmbr2  18685  lmmbrf  18688  iscau2  18703  iscau4  18705  caucfil  18709  lmclim  18728  bcthlem1  18746  bcth  18751  ishl2  18787  pmltpclem1  18808  elovolm  18834  ovolgelb  18839  ovolicc  18882  mbfaddlem  19015  i1fres  19060  mbfi1fseqlem4  19073  itg2l  19084  itg2leub  19089  itg2seq  19097  isibl  19120  iblitg  19123  dfitg  19124  itgeq2  19132  itgvallem  19139  iblcnlem1  19142  iblrelem  19145  iblpos  19147  ellimc3  19229  limciun  19244  limcun  19245  dvmptfsum  19322  dveflem  19326  lhop1lem  19360  dvfsumlem2  19374  dvfsumlem4  19376  mpfind  19428  pf1ind  19438  elply2  19578  plypf1  19594  coeval  19605  plydivlem4  19676  sincosq3sgn  19868  vmasum  20455  lgsqrlem1  20580  lgsquadlem1  20593  2sqlem8  20611  2sqlem9  20612  2sqlem11  20614  dchrisumlema  20637  dchrisumlem2  20639  pntibndlem3  20741  pntibnd  20742  pntleme  20757  pntlemp  20759  isgrpo  20863  isgrp2d  20902  isgrpda  20964  ismndo  21010  drngoi  21074  vci  21104  isvclem  21133  nmoofval  21340  nmooval  21341  nmosetn0  21343  nmoolb  21349  nmoubi  21350  nmoo0  21369  nmlno0lem  21371  isphg  21395  norm3lemt  21731  chlimi  21814  ocsh  21862  cmbr  22163  chscllem2  22217  spansncv  22232  eigorth  22418  nmopval  22436  nmopsetn0  22445  nmfnval  22456  nmfnsetn0  22458  nmoplb  22487  nmfnlb  22504  nmopnegi  22545  nmop0  22566  nmfn0  22567  nmlnop0iALT  22575  nmopun  22594  nmcexi  22606  branmfn  22685  leopmuli  22713  pjnmopi  22728  cvbr  22862  mdbr  22874  dmdbr  22879  atom1d  22933  chrelat2  22950  atcvati  22966  atord  22968  atcvat2  22969  chirredlem4  22973  mdsymlem5  22987  fmptcof2  23229  funcnv4mpt  23237  xeqlelt  23269  ishashinf  23389  esumcvg  23454  erdszelem3  23724  erdsze  23733  pconcn  23755  cnpcon  23761  txpcon  23763  conpcon  23766  cvmscbv  23789  iscvm  23790  cvmsi  23796  cvmsval  23797  iseupa  23881  eupath2lem3  23903  relexp0  24025  relexpsucr  24026  relexpsucl  24028  relexpadd  24035  relexpindlem  24036  mulle0b  24087  dfrdg2  24152  dfrdg3  24153  elpred  24177  trpredrec  24241  poseq  24253  soseq  24254  sltval  24301  nocvxminlem  24344  nofulllem1  24356  elfuns  24454  brimg  24476  brsuccf  24480  dfrdg4  24488  tfrqfree  24489  brcgr  24528  brbtwn2  24533  colinearalg  24538  ax5seg  24566  axcontlem5  24596  axcontlem10  24601  brofs  24628  funtransport  24654  fvtransport  24655  brifs  24666  lineext  24699  brfs  24702  btwnconn1lem11  24720  btwnconn1lem14  24723  brsegle  24731  segletr  24737  segleantisym  24738  seglelin  24739  funray  24763  fvray  24764  funline  24765  fvline  24767  ellines  24775  linethru  24776  areacirclem6  24930  rspc2edv  24963  eqvinopb  24965  repcpwti  25161  islatalg  25183  defge3  25271  prodeq2  25307  isfldOLD  25426  vecval1b  25451  vecval3b  25452  vri  25492  basexre  25522  sallnei  25529  osneisi  25531  flfnei2  25577  tcnvec  25690  ismgra  25710  isalg  25721  algi  25727  isded  25736  dedi  25737  cmpasso  25773  dualcat2  25784  isgraphmrph2  25924  domcatsetval2  25929  domcatval2  25931  codcatval2  25937  prismorcset3  25938  pgapspf2  26053  bisig0  26062  isig2a2  26066  isibg2  26110  isibg2aa  26112  isibg2aalem2  26114  pdiveql  26168  isibcg  26191  trer  26227  opnrebl2  26236  nn0prpwlem  26238  isfne4  26269  isfne2  26271  isfne3  26272  islocfin  26296  unirep  26349  fnopabeqd  26385  fdc  26455  fdc1  26456  istotbnd  26493  heibor1lem  26533  heibor  26545  isriscg  26615  iscringd  26624  isidlc  26640  prtlem16  26737  prtlem15  26743  ismrcd1  26773  ismrcd2  26774  mzpcompact2lem  26829  eldioph  26837  eldioph2  26841  eldioph2b  26842  eldioph3  26845  diophin  26852  diophun  26853  diophrex  26855  rexrabdioph  26875  fphpd  26899  fphpdo  26900  pellexlem3  26916  monotuz  27026  monotoddzzfi  27027  monotoddzz  27028  oddcomabszz  27029  jm2.27  27101  rmydioph  27107  expdiophlem1  27114  expdiophlem2  27115  aomclem6  27156  aomclem8  27159  islssfg  27168  islssfg2  27169  frlmup1  27250  hbtlem2  27328  hbtlem4  27330  hbtlem5  27332  hbtlem6  27333  dgraaval  27349  flcidc  27379  psgnunilem3  27419  psgneu  27429  psgnvali  27431  psgnvalii  27432  2sbc6g  27615  2sbc5g  27616  iotasbc2  27620  pm14.122a  27622  pm14.123a  27625  fmul01  27710  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  climmulf  27730  climexp  27731  climsuse  27734  climrecf  27735  climinff  27737  stoweidlem3  27752  stoweidlem4  27753  stoweidlem7  27756  stoweidlem15  27764  stoweidlem16  27765  stoweidlem17  27766  stoweidlem19  27768  stoweidlem20  27769  stoweidlem22  27771  stoweidlem23  27772  stoweidlem27  27776  stoweidlem30  27779  stoweidlem32  27781  stoweidlem34  27783  stoweidlem42  27791  stoweidlem43  27792  stoweidlem48  27797  stoweidlem51  27800  stoweidlem59  27808  2reu4a  27967  uvtx01vtx  28164  1vwmgra  28181  3vfriswmgra  28183  bnj976  28809  bnj852  28953  bnj1014  28992  bnj1015  28993  bnj1118  29014  bnj1123  29016  bnj1148  29026  bnj1171  29030  bnj1373  29060  bnj1489  29086  lsmsat  29198  lsmsatcv  29200  islshpat  29207  lcvfbr  29210  lcvbr  29211  lsatcv0  29221  islshpkrN  29310  cvrval  29459  cvrval2  29464  cvrnbtwn2  29465  cvlexch1  29518  hlsuprexch  29570  cvrval5  29604  cvrat  29611  cvrat42  29633  3dim0  29646  3dim2  29657  islpln3  29722  islpln5  29724  islvol3  29765  islvol5  29768  4atlem11  29798  lineset  29927  isline  29928  ispsubsp2  29935  isline2  29963  isline3  29965  elpaddat  29993  elpadd2at  29995  dalawlem15  30074  pclfinclN  30139  4atex  30265  4atex2  30266  4atex3  30270  ltrnu  30310  cdleme0nex  30479  cdleme31so  30568  cdleme31fv  30579  cdleme31fv2  30582  cdlemefrs29pre00  30584  cdlemefrs29cpre1  30587  cdlemftr3  30754  cdlemb3  30795  cdlemg6d  30810  cdlemg33b  30896  cdlemg33c  30897  cdlemg33e  30899  cdlemk42  31130  dvhopellsm  31307  dibelval3  31337  diblsmopel  31361  diclspsn  31384  dihval  31422  dihopelvalcpre  31438  dih1dimatlem  31519  dihglb2  31532  dochkrshp3  31578  dihjatcclem4  31611  dihjat1lem  31618  mapdval  31818  mapdpglem30  31892
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