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

Theorem anbi2d 686
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 24 . 2  |-  ( ph  ->  ( th  ->  ( ps 
<->  ch ) ) )
32pm5.32d 622 1  |-  ( ph  ->  ( ( th  /\  ps )  <->  ( th  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  anbi2  690  anbi12d  693  bi2anan9  845  2eu6  2368  eleq2  2499  ceqsex2  2994  ceqsex6v  2998  vtocl2gaf  3020  ceqsrex2v  3073  moeq3  3113  mob2  3116  eqreu  3128  nelrdva  3145  undif4  3686  r19.27z  3728  r19.27zv  3729  ssunsn2  3960  preq12bg  3979  opeq2  3987  ralunsn  4005  intab  4082  disjxun  4212  opabbid  4272  opthg  4438  pocl  4512  isso2i  4537  ordelord  4605  ordtri4  4620  dfwe2  4764  dflim4  4830  tfisi  4840  xpeq2  4895  rabxp  4916  vtoclr  4924  opeliunxp  4931  posn  4948  opbrop  4957  elrnmpt1  5121  dfres2  5195  brcodir  5255  poltletr  5271  xp11  5306  elxp4  5359  elxp5  5360  fununi  5519  fneq2  5537  fnun  5553  feq3  5580  foeq3  5653  funbrfv  5767  ssimaexg  5791  fvopab3g  5804  fvopab3ig  5805  fvelrn  5868  fmptco  5903  elunirnALT  6002  isoeq2  6042  isoeq3  6043  isoini  6060  isopolem  6067  f1oiso  6073  f1oiso2  6074  oprabbid  6129  cbvoprab3  6150  mpt2mptx  6166  mpt2fun  6174  ov  6195  ov3  6212  ov6g  6213  ovg  6214  caoftrn  6341  f1o2ndf1  6456  frxp  6458  xporderlem  6459  fnwelem  6463  brtpos2  6487  dftpos4  6500  riotabidv  6553  onfununi  6605  recseq  6636  tfrlem1  6638  omopth  6903  brecop  6999  eroveu  7001  erovlem  7002  erov  7003  ecopovtrn  7009  th3qlem1  7012  th3qlem2  7013  th3q  7015  elpmg  7034  ixpsnf1o  7104  domeng  7124  dom2lem  7149  xpcomco  7200  xpassen  7204  xpdom2  7205  omxpenlem  7211  xpf1o  7271  unxpdom  7318  isinf  7324  findcard2  7350  fiint  7385  supeq2  7455  inf0  7578  scott0  7812  isinffi  7881  isacn  7927  aceq1  8000  aceq0  8001  aceq2  8002  dfac3  8004  dfac5lem1  8006  dfac2  8013  dfac12lem2  8026  kmlem8  8039  kmlem14  8045  infmap2  8100  cfval  8129  cflim3  8144  sornom  8159  infpssrlem4  8188  isf32lem9  8243  domtriomlem  8324  axdc2lem  8330  zfac  8342  ac6num  8361  axrepndlem1  8469  axunndlem1  8472  axregnd  8481  axinfndlem1  8482  axacndlem4  8487  axacndlem5  8488  zfcndac  8496  fpwwe2lem5  8511  pwfseqlem4a  8538  pwfseqlem4  8539  alephgch  8555  wunex2  8615  tskord  8657  nqereu  8808  ordpipq  8821  prcdnq  8872  prnmax  8874  genpnnp  8884  distrlem5pr  8906  ltprord  8909  ltexprlem3  8917  ltexprlem4  8918  ltexpri  8922  prlem936  8926  reclem2pr  8927  ltsosr  8971  mulgt0sr  8982  ltresr  9017  axpre-lttrn  9043  axpre-mulgt0  9045  eqlelt  9164  lesub0  9546  wloglei  9561  sup3  9967  infm3  9969  prime  10352  fzind  10370  uzwo  10541  uzwoOLD  10542  zbtwnre  10574  xltnegi  10804  xmulneg1  10850  ixxval  10926  fzval  11047  elfzm11  11118  elfzo  11144  seqof2  11383  nn0opth2  11567  facwordi  11582  hashnn0n0nn  11666  brfi1uzind  11717  shftfval  11887  shftfib  11889  shftfn  11890  2shfti  11897  abs1m  12141  cau3lem  12160  caubnd2  12163  clim  12290  rlim  12291  clim2  12300  climi  12306  o1lo1  12333  rlimcn2  12386  climcn2  12388  addcn2  12389  subcn2  12390  mulcn2  12391  o1of2  12408  isercoll  12463  caurcvg2  12473  sumeq2w  12488  sumeq2ii  12489  cbvsum  12491  summo  12513  fsum  12516  sinbnd  12783  cosbnd  12784  divalgb  12926  ndvdssub  12929  smupp1  12994  smueqlem  13004  gcdval  13010  gcdcllem2  13014  gcdneg  13028  gcdass  13047  algcvgblem  13070  prmind2  13092  qredeq  13108  euclemma  13110  qnumval  13131  qdenval  13132  eulerthlem2  13173  pceu  13222  pczpre  13223  pcdiv  13228  prmpwdvds  13274  prmreclem5  13290  vdwapun  13344  ramub2  13384  rami  13385  ramcl  13399  ismred2  13830  isacs  13878  iscatd2  13908  catpropd  13937  oppccatid  13947  isinv  13987  isssc  14022  funcres2b  14096  funcpropd  14099  fucinv  14172  yoniso  14384  prslem  14390  drsdir  14394  drsdirfi  14397  posi  14409  isposd  14414  pltval  14419  plttr  14429  isipodrs  14589  ipodrsima  14593  spwval  14659  dirge  14684  mndlem1  14696  gsumpropd  14778  gsumress  14779  divsgrp2  14938  resscntz  15132  isslw  15244  subgslw  15252  iscmnd  15426  gsumval3eu  15515  gsumval3  15516  dmdprd  15561  subgdmdprd  15594  dprd2d2  15604  pgpfac1  15640  pgpfaclem2  15642  pgpfaclem3  15643  pgpfac  15644  ablfaclem1  15645  divsrng2  15728  dvdsrval  15752  crngunit  15769  dfrhm2  15823  isdrngd  15862  abvpropd  15932  islmod  15956  lssacs  16045  lsspropd  16095  islmhm  16105  lbspropd  16173  fiidomfld  16370  ltbval  16534  opsrval  16537  pjfval2  16938  eltopspOLD  16985  istpsOLD  16987  basis2  17018  eltg2  17025  isclo  17153  isnei  17169  isneip  17171  neiptopnei  17198  restbas  17224  restcld  17238  neitr  17246  iscnp  17303  iscnp3  17310  tgcn  17318  cnpimaex  17322  lmbrf  17326  cncnp  17346  cnprest2  17356  isreg  17398  regsep  17400  isnrm  17401  ist1-2  17413  nrmsep3  17421  isnrm2  17424  hauscmplem  17471  dfcon2  17484  is1stc  17506  1stcclb  17509  1stcfb  17510  is2ndc  17511  2ndc1stc  17516  1stcrest  17518  2ndcsep  17524  1stccnp  17527  islly  17533  llyeq  17535  llyi  17539  hausllycmp  17559  lly1stc  17561  txbas  17601  ptpjpre1  17605  elpt  17606  txcnpi  17642  ptpjopn  17646  ptcldmpt  17648  ptclsg  17649  txcnp  17654  ptcnp  17656  hausdiag  17679  tx1stc  17684  xkoinjcn  17721  imasnopn  17724  imasncld  17725  imasncls  17726  fbfinnfr  17875  snfil  17898  uffix2  17958  elfm  17981  elfm2  17982  fmco  17995  hauspwpwf1  18021  flfnei  18025  isflf  18027  lmflf  18039  fclscf  18059  isfcf  18068  alexsublem  18077  cnextcn  18100  cnextfres  18101  eltsms  18164  tsmsres  18175  tsmsf1o  18176  ustuqtop4  18276  ispsmet  18337  ismet  18355  isxmet  18356  ismet2  18365  imasdsf1olem  18405  blres  18463  met2ndc  18555  metcnp3  18572  nrmmetd  18624  pi1grplem  19076  lmmbr2  19214  lmmbrf  19217  iscau2  19232  iscau4  19234  caucfil  19238  lmclim  19257  cfilucfil3OLD  19273  cfilucfil3  19274  bcthlem1  19279  bcth  19284  ishl2  19326  pmltpclem1  19347  elovolm  19373  ovolgelb  19378  ovolicc  19421  mbfaddlem  19554  i1fres  19599  mbfi1fseqlem4  19612  itg2l  19623  itg2leub  19628  itg2seq  19636  isibl  19659  iblitg  19662  dfitg  19663  itgeq2  19671  itgvallem  19678  iblcnlem1  19681  iblrelem  19684  iblpos  19686  ellimc3  19768  limciun  19783  limcun  19784  dvmptfsum  19861  dveflem  19865  lhop1lem  19899  dvfsumlem2  19913  dvfsumlem4  19915  mpfind  19967  pf1ind  19977  elply2  20117  plypf1  20133  coeval  20144  plydivlem4  20215  sincosq3sgn  20410  vmasum  21002  lgsqrlem1  21127  lgsquadlem1  21140  2sqlem8  21158  2sqlem9  21159  2sqlem11  21161  dchrisumlema  21184  dchrisumlem2  21186  pntibndlem3  21288  pntibnd  21289  pntleme  21304  pntlemp  21306  usgraedg4  21408  cusgrafilem2  21491  cusgrafi  21493  uvtx01vtx  21503  usgrnloop  21565  spthonepeq  21589  usgrcyclnl2  21630  4cycl4v4e  21655  4cycl4dv4e  21657  iseupa  21689  eupath2lem3  21703  isgrpo  21786  isgrp2d  21825  isgrpda  21887  ismndo  21933  drngoi  21997  vci  22029  isvclem  22058  nmoofval  22265  nmooval  22266  nmosetn0  22268  nmoolb  22274  nmoubi  22275  nmoo0  22294  nmlno0lem  22296  isphg  22320  norm3lemt  22656  chlimi  22739  ocsh  22787  cmbr  23088  chscllem2  23142  spansncv  23157  eigorth  23343  nmopval  23361  nmopsetn0  23370  nmfnval  23381  nmfnsetn0  23383  nmoplb  23412  nmfnlb  23429  nmopnegi  23470  nmop0  23491  nmfn0  23492  nmlnop0iALT  23500  nmopun  23519  nmcexi  23531  branmfn  23610  leopmuli  23638  pjnmopi  23653  cvbr  23787  mdbr  23799  dmdbr  23804  atom1d  23858  chrelat2  23875  atcvati  23891  atord  23893  atcvat2  23894  chirredlem4  23898  mdsymlem5  23912  fmptcof2  24078  ofpreima  24083  funcnv4mpt  24087  2ndpreima  24098  xeqlelt  24141  ishashinf  24161  isofld  24237  ofldadd  24240  ofldmul  24241  esumcvg  24478  sitgval  24649  lgamgulmlem2  24816  erdszelem3  24881  erdsze  24890  pconcn  24913  cnpcon  24919  txpcon  24921  conpcon  24924  cvmscbv  24947  iscvm  24948  cvmsi  24954  cvmsval  24955  relexp0  25131  relexpsucr  25132  relexpsucl  25134  relexpadd  25140  relexpindlem  25141  mulle0b  25194  prodfdiv  25226  ntrivcvgn0  25228  ntrivcvgmullem  25231  prodeq1f  25236  prodeq2w  25240  prodeq2ii  25241  prodmo  25264  zprod  25265  fprod  25269  fprodntriv  25270  elima4  25406  dfrdg2  25425  dfrdg3  25426  elpred  25454  trpredrec  25518  poseq  25530  soseq  25531  sltval  25604  nocvxminlem  25647  nofulllem1  25659  elfuns  25762  brimg  25784  brsuccf  25788  dfrdg4  25797  tfrqfree  25798  brcgr  25841  brbtwn2  25846  colinearalg  25851  ax5seg  25879  axcontlem5  25909  axcontlem10  25914  brofs  25941  funtransport  25967  fvtransport  25968  brifs  25979  lineext  26012  brfs  26015  btwnconn1lem11  26033  btwnconn1lem14  26036  brsegle  26044  segletr  26050  segleantisym  26051  seglelin  26052  funray  26076  fvray  26077  funline  26078  fvline  26080  ellines  26088  linethru  26089  mblfinlem3  26247  mblfinlem4  26248  ismblfin  26249  mbfresfi  26255  itg2addnclem  26258  itg2addnclem3  26260  itg2addnc  26261  ftc1anclem7  26288  ftc1anc  26290  areacirclem5  26298  trer  26321  opnrebl2  26326  nn0prpwlem  26327  isfne4  26351  isfne2  26353  isfne3  26354  islocfin  26378  unirep  26416  fnopabeqd  26423  fdc  26451  fdc1  26452  istotbnd  26480  heibor1lem  26520  heibor  26532  isriscg  26602  iscringd  26611  isidlc  26627  prtlem16  26720  prtlem15  26726  ismrcd1  26754  ismrcd2  26755  mzpcompact2lem  26810  eldioph  26818  eldioph2  26822  eldioph2b  26823  eldioph3  26826  diophin  26833  diophun  26834  diophrex  26836  rexrabdioph  26856  fphpd  26879  fphpdo  26880  pellexlem3  26896  monotuz  27006  monotoddzzfi  27007  monotoddzz  27008  oddcomabszz  27009  jm2.27  27081  rmydioph  27087  expdiophlem1  27094  expdiophlem2  27095  aomclem6  27136  aomclem8  27138  islssfg  27147  islssfg2  27148  frlmup1  27229  hbtlem2  27307  hbtlem4  27309  hbtlem5  27311  hbtlem6  27312  dgraaval  27328  flcidc  27358  psgnunilem3  27398  psgneu  27408  psgnvali  27410  psgnvalii  27411  2sbc6g  27594  2sbc5g  27595  iotasbc2  27599  pm14.122a  27601  pm14.123a  27604  fmul01  27688  fmuldfeqlem1  27690  fmuldfeq  27691  fmul01lt1lem1  27692  fmul01lt1lem2  27693  climmulf  27708  climexp  27709  climsuse  27712  climrecf  27713  climinff  27715  stoweidlem3  27730  stoweidlem4  27731  stoweidlem7  27734  stoweidlem15  27742  stoweidlem16  27743  stoweidlem17  27744  stoweidlem19  27746  stoweidlem20  27747  stoweidlem22  27749  stoweidlem23  27750  stoweidlem27  27754  stoweidlem30  27757  stoweidlem32  27759  stoweidlem34  27761  stoweidlem42  27769  stoweidlem43  27770  stoweidlem48  27775  stoweidlem51  27778  stoweidlem59  27786  stoweidlem60  27787  2reu4a  27945  f12dfv  28086  f13dfv  28087  oprabv  28091  swrdccatin1d  28242  swrdccatin2d  28243  swrdccatin12d  28244  usgra2wlkspthlem1  28332  wwlk  28351  wlklniswwlkn2  28370  el2wlkonot  28389  el2spthonot  28390  el2spthonot0  28391  usg2spthonot  28408  usg2spthonot0  28409  usg2spthonot1  28410  isrusgra  28430  1vwmgra  28455  3vfriswmgra  28457  3cyclfrgrarn1  28464  4cycl2vnunb  28469  vdn1frgrav2  28478  vdgn1frgrav2  28479  frgrancvvdeqlemB  28489  usg2spot2nb  28516  usgreg2spot  28518  2spotmdisj  28519  usgreghash2spot  28520  bnj976  29210  bnj852  29354  bnj1014  29393  bnj1015  29394  bnj1118  29415  bnj1123  29417  bnj1148  29427  bnj1171  29431  bnj1373  29461  bnj1489  29487  lsmsat  29868  lsmsatcv  29870  islshpat  29877  lcvfbr  29880  lcvbr  29881  lsatcv0  29891  islshpkrN  29980  cvrval  30129  cvrval2  30134  cvrnbtwn2  30135  cvlexch1  30188  hlsuprexch  30240  cvrval5  30274  cvrat  30281  cvrat42  30303  3dim0  30316  3dim2  30327  islpln3  30392  islpln5  30394  islvol3  30435  islvol5  30438  4atlem11  30468  lineset  30597  isline  30598  ispsubsp2  30605  isline2  30633  isline3  30635  elpaddat  30663  elpadd2at  30665  dalawlem15  30744  pclfinclN  30809  4atex  30935  4atex2  30936  4atex3  30940  ltrnu  30980  cdleme0nex  31149  cdleme31so  31238  cdleme31fv  31249  cdleme31fv2  31252  cdlemefrs29pre00  31254  cdlemefrs29cpre1  31257  cdlemftr3  31424  cdlemb3  31465  cdlemg6d  31480  cdlemg33b  31566  cdlemg33c  31567  cdlemg33e  31569  cdlemk42  31800  dvhopellsm  31977  dibelval3  32007  diblsmopel  32031  diclspsn  32054  dihval  32092  dihopelvalcpre  32108  dih1dimatlem  32189  dihglb2  32202  dochkrshp3  32248  dihjatcclem4  32281  dihjat1lem  32288  mapdval  32488  mapdpglem30  32562
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 179  df-an 362
  Copyright terms: Public domain W3C validator