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  2241  eleq2  2357  ceqsex2  2837  ceqsex6v  2841  vtocl2gaf  2863  ceqsrex2v  2916  moeq3  2955  mob2  2958  eqreu  2970  undif4  3524  r19.27z  3565  r19.27zv  3566  ssunsn2  3789  preq12bg  3807  opeq2  3813  ralunsn  3831  intab  3908  disjxun  4037  opabbid  4097  opthg  4262  pocl  4337  isso2i  4362  ordelord  4430  ordtri4  4445  dfwe2  4589  dflim4  4655  tfisi  4665  xpeq2  4720  rabxp  4741  vtoclr  4749  opeliunxp  4756  posn  4774  opbrop  4783  elrnmpt1  4944  dfres2  5018  brcodir  5078  poltletr  5094  xp11  5127  elxp4  5176  elxp5  5177  fununi  5332  fneq2  5350  fnun  5366  feq3  5393  foeq3  5465  funbrfv  5577  ssimaexg  5601  fvopab3g  5614  fvopab3ig  5615  fvelrn  5677  fmptco  5707  elunirnALT  5795  isoeq2  5833  isoeq3  5834  isoini  5851  isopolem  5858  f1oiso  5864  f1oiso2  5865  oprabbid  5917  cbvoprab3  5938  mpt2mptx  5954  mpt2fun  5962  ov  5983  ov3  6000  ov6g  6001  ovg  6002  caoftrn  6128  frxp  6241  xporderlem  6242  fnwelem  6246  brtpos2  6256  dftpos4  6269  riotabidv  6322  onfununi  6374  recseq  6405  tfrlem1  6407  omopth  6672  brecop  6767  eroveu  6769  erovlem  6770  erov  6771  ecopovtrn  6777  th3qlem1  6780  th3qlem2  6781  th3q  6783  elpmg  6802  ixpsnf1o  6872  domeng  6892  dom2lem  6917  xpcomco  6968  xpassen  6972  xpdom2  6973  omxpenlem  6979  xpf1o  7039  unxpdom  7086  isinf  7092  findcard2  7114  fiint  7149  supeq2  7217  inf0  7338  scott0  7572  isinffi  7641  isacn  7687  aceq1  7760  aceq0  7761  aceq2  7762  dfac3  7764  dfac5lem1  7766  dfac2  7773  dfac12lem2  7786  kmlem8  7799  kmlem14  7805  infmap2  7860  cfval  7889  cflim3  7904  sornom  7919  infpssrlem4  7948  isf32lem9  8003  domtriomlem  8084  axdc2lem  8090  zfac  8102  ac6num  8122  axrepndlem1  8230  axunndlem1  8233  axregnd  8242  axinfndlem1  8243  axacndlem4  8248  axacndlem5  8249  zfcndac  8257  fpwwe2lem5  8272  pwfseqlem4a  8299  pwfseqlem4  8300  alephgch  8316  wunex2  8376  tskord  8418  nqereu  8569  ordpipq  8582  prcdnq  8633  prnmax  8635  genpnnp  8645  distrlem5pr  8667  ltprord  8670  ltexprlem3  8678  ltexprlem4  8679  ltexpri  8683  prlem936  8687  reclem2pr  8688  ltsosr  8732  mulgt0sr  8743  ltresr  8778  axpre-lttrn  8804  axpre-mulgt0  8806  eqlelt  8925  lesub0  9306  wloglei  9321  sup3  9727  infm3  9729  prime  10108  fzind  10126  uzwo  10297  uzwoOLD  10298  zbtwnre  10330  xltnegi  10559  xmulneg1  10605  ixxval  10680  fzval  10800  elfzm11  10869  elfzo  10893  nn0opth2  11303  facwordi  11318  shftfval  11581  shftfib  11583  shftfn  11584  2shfti  11591  abs1m  11835  cau3lem  11854  caubnd2  11857  clim  11984  rlim  11985  clim2  11994  climi  12000  o1lo1  12027  rlimcn2  12080  climcn2  12082  addcn2  12083  subcn2  12084  mulcn2  12085  o1of2  12102  isercoll  12157  caurcvg2  12166  sumeq2w  12181  sumeq2ii  12182  cbvsum  12184  summo  12206  fsum  12209  sinbnd  12476  cosbnd  12477  divalgb  12619  ndvdssub  12622  smupp1  12687  smueqlem  12697  gcdval  12703  gcdcllem2  12707  gcdneg  12721  gcdass  12740  algcvgblem  12763  prmind2  12785  qredeq  12801  euclemma  12803  qnumval  12824  qdenval  12825  eulerthlem2  12866  pceu  12915  pczpre  12916  pcdiv  12921  prmpwdvds  12967  prmreclem5  12983  vdwapun  13037  ramub2  13077  rami  13078  ramcl  13092  ismred2  13521  isacs  13569  iscatd2  13599  catpropd  13628  oppccatid  13638  isinv  13678  isssc  13713  funcres2b  13787  funcpropd  13790  fucinv  13863  yoniso  14075  prslem  14081  drsdir  14085  drsdirfi  14088  posi  14100  isposd  14105  pltval  14110  plttr  14120  isipodrs  14280  ipodrsima  14284  spwval  14350  dirge  14375  mndlem1  14387  gsumpropd  14469  gsumress  14470  divsgrp2  14629  resscntz  14823  isslw  14935  subgslw  14943  iscmnd  15117  gsumval3eu  15206  gsumval3  15207  dmdprd  15252  subgdmdprd  15285  dprd2d2  15295  pgpfac1  15331  pgpfaclem2  15333  pgpfaclem3  15334  pgpfac  15335  ablfaclem1  15336  divsrng2  15419  dvdsrval  15443  crngunit  15460  dfrhm2  15514  isdrngd  15553  abvpropd  15623  islmod  15647  lssacs  15740  lsspropd  15790  islmhm  15800  lbspropd  15868  fiidomfld  16065  ltbval  16229  opsrval  16232  pjfval2  16625  eltopspOLD  16672  istpsOLD  16674  basis2  16705  eltg2  16712  isclo  16840  isnei  16856  isneip  16858  restbas  16905  restcld  16919  iscnp  16983  iscnp3  16990  tgcn  16998  cnpimaex  17002  lmbrf  17006  cncnp  17025  cnprest2  17034  isreg  17076  regsep  17078  isnrm  17079  ist1-2  17091  nrmsep3  17099  isnrm2  17102  hauscmplem  17149  dfcon2  17161  is1stc  17183  1stcclb  17186  1stcfb  17187  is2ndc  17188  2ndc1stc  17193  1stcrest  17195  2ndcsep  17201  1stccnp  17204  islly  17210  llyeq  17212  llyi  17216  hausllycmp  17236  lly1stc  17238  txbas  17278  ptpjpre1  17282  elpt  17283  txcnpi  17318  ptpjopn  17322  ptcldmpt  17324  ptclsg  17325  txcnp  17330  ptcnp  17332  hausdiag  17355  tx1stc  17360  xkoinjcn  17397  fbfinnfr  17552  snfil  17575  uffix2  17635  elfm  17658  elfm2  17659  fmco  17672  hauspwpwf1  17698  flfnei  17702  isflf  17704  lmflf  17716  fclscf  17736  isfcf  17745  alexsublem  17754  eltsms  17831  tsmsres  17842  tsmsf1o  17843  ismet  17904  isxmet  17905  ismet2  17914  imasdsf1olem  17953  blres  17993  met2ndc  18085  metcnp3  18102  nrmmetd  18113  pi1grplem  18563  lmmbr2  18701  lmmbrf  18704  iscau2  18719  iscau4  18721  caucfil  18725  lmclim  18744  bcthlem1  18762  bcth  18767  ishl2  18803  pmltpclem1  18824  elovolm  18850  ovolgelb  18855  ovolicc  18898  mbfaddlem  19031  i1fres  19076  mbfi1fseqlem4  19089  itg2l  19100  itg2leub  19105  itg2seq  19113  isibl  19136  iblitg  19139  dfitg  19140  itgeq2  19148  itgvallem  19155  iblcnlem1  19158  iblrelem  19161  iblpos  19163  ellimc3  19245  limciun  19260  limcun  19261  dvmptfsum  19338  dveflem  19342  lhop1lem  19376  dvfsumlem2  19390  dvfsumlem4  19392  mpfind  19444  pf1ind  19454  elply2  19594  plypf1  19610  coeval  19621  plydivlem4  19692  sincosq3sgn  19884  vmasum  20471  lgsqrlem1  20596  lgsquadlem1  20609  2sqlem8  20627  2sqlem9  20628  2sqlem11  20630  dchrisumlema  20653  dchrisumlem2  20655  pntibndlem3  20757  pntibnd  20758  pntleme  20773  pntlemp  20775  isgrpo  20879  isgrp2d  20918  isgrpda  20980  ismndo  21026  drngoi  21090  vci  21120  isvclem  21149  nmoofval  21356  nmooval  21357  nmosetn0  21359  nmoolb  21365  nmoubi  21366  nmoo0  21385  nmlno0lem  21387  isphg  21411  norm3lemt  21747  chlimi  21830  ocsh  21878  cmbr  22179  chscllem2  22233  spansncv  22248  eigorth  22434  nmopval  22452  nmopsetn0  22461  nmfnval  22472  nmfnsetn0  22474  nmoplb  22503  nmfnlb  22520  nmopnegi  22561  nmop0  22582  nmfn0  22583  nmlnop0iALT  22591  nmopun  22610  nmcexi  22622  branmfn  22701  leopmuli  22729  pjnmopi  22744  cvbr  22878  mdbr  22890  dmdbr  22895  atom1d  22949  chrelat2  22966  atcvati  22982  atord  22984  atcvat2  22985  chirredlem4  22989  mdsymlem5  23003  fmptcof2  23244  funcnv4mpt  23252  xeqlelt  23284  ishashinf  23404  esumcvg  23469  erdszelem3  23739  erdsze  23748  pconcn  23770  cnpcon  23776  txpcon  23778  conpcon  23781  cvmscbv  23804  iscvm  23805  cvmsi  23811  cvmsval  23812  iseupa  23896  eupath2lem3  23918  relexp0  24040  relexpsucr  24041  relexpsucl  24043  relexpadd  24050  relexpindlem  24051  mulle0b  24102  cprodeq1f  24130  cprodeq2w  24134  cprodeq2ii  24135  prodmo  24159  zprod  24160  zprodn0  24162  fprod  24164  dfrdg2  24223  dfrdg3  24224  elpred  24248  trpredrec  24312  poseq  24324  soseq  24325  sltval  24372  nocvxminlem  24415  nofulllem1  24427  elfuns  24525  brimg  24547  brsuccf  24551  dfrdg4  24560  tfrqfree  24561  brcgr  24600  brbtwn2  24605  colinearalg  24610  ax5seg  24638  axcontlem5  24668  axcontlem10  24673  brofs  24700  funtransport  24726  fvtransport  24727  brifs  24738  lineext  24771  brfs  24774  btwnconn1lem11  24792  btwnconn1lem14  24795  brsegle  24803  segletr  24809  segleantisym  24810  seglelin  24811  funray  24835  fvray  24836  funline  24837  fvline  24839  ellines  24847  linethru  24848  itg2addnclem  25003  itg2addnc  25005  areacirclem6  25033  rspc2edv  25066  eqvinopb  25068  repcpwti  25264  islatalg  25286  defge3  25374  prodeq2  25410  isfldOLD  25529  vecval1b  25554  vecval3b  25555  vri  25595  basexre  25625  sallnei  25632  osneisi  25634  flfnei2  25680  tcnvec  25793  ismgra  25813  isalg  25824  algi  25830  isded  25839  dedi  25840  cmpasso  25876  dualcat2  25887  isgraphmrph2  26027  domcatsetval2  26032  domcatval2  26034  codcatval2  26040  prismorcset3  26041  pgapspf2  26156  bisig0  26165  isig2a2  26169  isibg2  26213  isibg2aa  26215  isibg2aalem2  26217  pdiveql  26271  isibcg  26294  trer  26330  opnrebl2  26339  nn0prpwlem  26341  isfne4  26372  isfne2  26374  isfne3  26375  islocfin  26399  unirep  26452  fnopabeqd  26488  fdc  26558  fdc1  26559  istotbnd  26596  heibor1lem  26636  heibor  26648  isriscg  26718  iscringd  26727  isidlc  26743  prtlem16  26840  prtlem15  26846  ismrcd1  26876  ismrcd2  26877  mzpcompact2lem  26932  eldioph  26940  eldioph2  26944  eldioph2b  26945  eldioph3  26948  diophin  26955  diophun  26956  diophrex  26958  rexrabdioph  26978  fphpd  27002  fphpdo  27003  pellexlem3  27019  monotuz  27129  monotoddzzfi  27130  monotoddzz  27131  oddcomabszz  27132  jm2.27  27204  rmydioph  27210  expdiophlem1  27217  expdiophlem2  27218  aomclem6  27259  aomclem8  27262  islssfg  27271  islssfg2  27272  frlmup1  27353  hbtlem2  27431  hbtlem4  27433  hbtlem5  27435  hbtlem6  27436  dgraaval  27452  flcidc  27482  psgnunilem3  27522  psgneu  27532  psgnvali  27534  psgnvalii  27535  2sbc6g  27718  2sbc5g  27719  iotasbc2  27723  pm14.122a  27725  pm14.123a  27728  fmul01  27813  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  climmulf  27833  climexp  27834  climsuse  27837  climrecf  27838  climinff  27840  stoweidlem3  27855  stoweidlem4  27856  stoweidlem7  27859  stoweidlem15  27867  stoweidlem16  27868  stoweidlem17  27869  stoweidlem19  27871  stoweidlem20  27872  stoweidlem22  27874  stoweidlem23  27875  stoweidlem27  27879  stoweidlem30  27882  stoweidlem32  27884  stoweidlem34  27886  stoweidlem42  27894  stoweidlem43  27895  stoweidlem48  27900  stoweidlem51  27903  stoweidlem59  27911  2reu4a  28070  uvtx01vtx  28305  usgrnloop  28351  usgrcyclnl2  28387  4cycl4v4e  28412  4cycl4dv4e  28414  1vwmgra  28427  3vfriswmgra  28429  3cyclfrgrarn1  28435  4cycl2vnunb  28439  bnj976  29125  bnj852  29269  bnj1014  29308  bnj1015  29309  bnj1118  29330  bnj1123  29332  bnj1148  29342  bnj1171  29346  bnj1373  29376  bnj1489  29402  lsmsat  29820  lsmsatcv  29822  islshpat  29829  lcvfbr  29832  lcvbr  29833  lsatcv0  29843  islshpkrN  29932  cvrval  30081  cvrval2  30086  cvrnbtwn2  30087  cvlexch1  30140  hlsuprexch  30192  cvrval5  30226  cvrat  30233  cvrat42  30255  3dim0  30268  3dim2  30279  islpln3  30344  islpln5  30346  islvol3  30387  islvol5  30390  4atlem11  30420  lineset  30549  isline  30550  ispsubsp2  30557  isline2  30585  isline3  30587  elpaddat  30615  elpadd2at  30617  dalawlem15  30696  pclfinclN  30761  4atex  30887  4atex2  30888  4atex3  30892  ltrnu  30932  cdleme0nex  31101  cdleme31so  31190  cdleme31fv  31201  cdleme31fv2  31204  cdlemefrs29pre00  31206  cdlemefrs29cpre1  31209  cdlemftr3  31376  cdlemb3  31417  cdlemg6d  31432  cdlemg33b  31518  cdlemg33c  31519  cdlemg33e  31521  cdlemk42  31752  dvhopellsm  31929  dibelval3  31959  diblsmopel  31983  diclspsn  32006  dihval  32044  dihopelvalcpre  32060  dih1dimatlem  32141  dihglb2  32154  dochkrshp3  32200  dihjatcclem4  32233  dihjat1lem  32240  mapdval  32440  mapdpglem30  32514
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