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

Theorem anbi2i 676
Description: Introduce 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
bi.aa  |-  ( ph  <->  ps )
Assertion
Ref Expression
anbi2i  |-  ( ( ch  /\  ph )  <->  ( ch  /\  ps )
)

Proof of Theorem anbi2i
StepHypRef Expression
1 bi.aa . . 3  |-  ( ph  <->  ps )
21a1i 11 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
32pm5.32i 619 1  |-  ( ( ch  /\  ph )  <->  ( ch  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  anbi12i  679  an4  798  an42  799  anandir  803  dfbi3  864  dn1  933  nannan  1297  cadan  1398  cadcoma  1401  nic-mpALT  1443  nic-axALT  1445  19.35  1607  19.27  1831  19.41  1889  3exdistr  1922  4exdistr  1923  4exdistrOLD  1924  sb6  2134  2sb5  2147  2sb5rf  2153  sbel2x  2161  eu2  2265  eu3  2266  mo4f  2272  eu5  2278  eu4  2279  euan  2297  2mos  2319  2eu4  2323  2eu6  2325  clelab  2509  nonconne  2559  r2exf  2687  ceqsex3v  2939  ceqsex4v  2940  ceqsex8v  2942  reu2  3067  reu6  3068  reu4  3073  reu7  3074  2reu5lem3  3086  2reu5  3087  rmo3  3193  dfpss2  3377  difdif  3418  raldifb  3432  inass  3496  dfss4  3520  dfin2  3522  indi  3532  indifdir  3542  difin0ss  3639  inssdif0  3640  ssunpr  3906  unipr  3973  uniun  3978  uniin  3979  iunin2  4098  iundif2  4101  iindif2  4103  iinin2  4104  axrep1  4264  axrep4  4267  notzfaus  4317  eqvinop  4384  opcom  4393  opeqsn  4395  ordtri3or  4556  uniuni  4658  reusv2lem4  4669  tfindsg  4782  findsg  4814  fconstmpt  4863  opeliunxp  4871  xpundi  4872  elvvv  4879  xpiindi  4952  elcnv2  4992  cnvuni  4999  dmuni  5021  opelres  5093  elima3  5152  imai  5160  imainss  5229  ssrnres  5251  cnvresima  5301  mptpreima  5305  coundir  5314  rnco  5318  coass  5330  relrelss  5335  dffun2  5406  dffun3  5407  dffun4  5408  dffun5  5409  dffun6f  5410  dffun7  5421  dffun8  5422  dffun9  5423  svrelfun  5456  fncnv  5457  funcnvuni  5460  imadif  5470  dfmpt3  5509  fint  5564  fin  5565  dff12  5580  fores  5604  dff1o4  5624  eqfnfv3  5770  fndmin  5778  fniniseg  5792  rexsupp  5796  unpreima  5797  ffnfvf  5836  fsn2  5849  opabex3d  5930  opabex3  5931  dff13f  5947  isocnv2  5992  ffnov  6115  eqfnov  6117  foov  6161  difxp  6321  frxp  6394  soxp  6397  mpt2xopovel  6409  brtpos  6426  tpostpos  6437  dfsmo2  6547  tfrlem2  6575  rdglem1  6611  tz7.49  6640  brwitnlem  6689  oeeu  6784  erinxp  6916  mapsncnv  6998  cbvixp  7017  ixpin  7025  ixpiin  7026  mptelixpg  7037  elixpsn  7039  ixpsnf1o  7040  mapsnen  7122  xpassen  7140  omxpenlem  7147  sbthcl  7167  dfsup2OLD  7385  wemapso2lem  7454  dford2  7510  inf2  7513  zfinf  7529  trcl  7599  iscard2  7798  leweon  7828  aceq1  7933  dfac3  7937  dfac4  7938  dfac5lem2  7940  dfac5lem3  7941  dfac5  7944  kmlem3  7967  kmlem4  7968  kmlem14  7978  kmlem15  7979  dfackm  7981  infmap2  8033  cf0  8066  fin23lem25  8139  zorn2lem7  8317  brdom6disj  8345  zfcndrep  8424  zfcndinf  8428  fpwwe  8456  axgroth4  8642  grothprim  8644  grothtsk  8645  nqpr  8826  opelreal  8940  elnnz  10226  elznn0nn  10229  peano2uz2  10291  nnwos  10478  dflt2  10675  xmullem  10777  elfzuzb  10987  4fvwrd4  11053  fzm1  11059  elfznelfzo  11121  fzind2  11127  hashinfxadd  11588  hashfun  11629  brfi1uzind  11644  shftdm  11815  rexfiuz  12080  mertenslem2  12591  mertens  12592  divalglem10  12851  ndvdssub  12856  bitsmod  12877  algcvgblem  12997  isprm2  13016  isprm4  13018  hashdvds  13093  infpn2  13210  hashbc0  13302  xpscf  13720  funcpropd  14026  isffth2  14042  eldmcoa  14149  setcinv  14174  xpccatid  14214  yonedainv  14307  ispos  14333  ispos2  14334  istsr2  14579  spwmo  14587  isnsg2  14899  isnsg4  14912  isgim  14978  oppgid  15081  oppgcntz  15089  efgval2  15285  iscyg2  15421  dmdprdd  15489  subgdmdprd  15521  oppr1  15668  opprunit  15695  opprirred  15736  isrhm  15753  subsubrg2  15824  islmim  16063  lbsextg  16163  lidlnz  16228  isdomn2  16288  opsrtoslem1  16473  unocv  16832  pjfval2  16861  istop2g  16894  istps4OLD  16913  isbasis2g  16938  tgval2  16946  isclo2  17077  isnrm2  17346  is1stc2  17428  llyi  17460  isfbas2  17790  elfg  17826  ufinffr  17884  isfcls  17964  alexsubALTlem2  18002  alexsubALTlem3  18003  cnextcn  18021  ustfilxp  18165  iscusp2  18255  elcncf1di  18798  tchcph  19067  iscau3  19104  caucfil  19109  ellogdm  20399  dvdsflsumcom  20842  logfac2  20870  dchrelbas3  20891  dchrvmasumlema  21063  nb3grapr2  21331  uvtx01vtx  21369  3v3e3cycl2  21501  isgrpo2  21635  hhcms  22555  isch3  22594  ocsh  22635  pjhtheu  22746  pjpreeq  22750  h1deoi  22901  h1dei  22902  eleigvec  23310  cvbr2  23636  cvnbtwn2  23640  cvnbtwn4  23642  mdsl2i  23675  cvmdi  23677  mdsymlem6  23761  cdj3lem3b  23793  mo5f  23818  nmo  23819  rexunirn  23824  rmo3f  23828  rmo4fOLD  23829  rmo4f  23830  unipreima  23900  1stpreima  23938  isrnsigaOLD  24293  isrnsiga  24294  ballotlemodife  24536  erdszelem9  24666  cvmlift2lem9  24779  cvmlift2lem13  24783  axinfprim  24936  axacprim  24937  cbvprod  25022  prodmo  25043  iprodmul  25090  coep  25134  dfso2  25137  dford5reg  25164  dfon2lem5  25169  dfon2  25174  preduz  25226  wfi  25233  trpredmintr  25260  frind  25269  tfrALTlem  25302  frr3g  25306  brtxp2  25447  brpprod3a  25452  elfix  25469  dffix2  25471  dfom5b  25478  dffun10  25479  elfuns  25480  brcart  25497  brimg  25502  brsuccf  25506  funpartlem  25507  axcontlem5  25623  axcontlem6  25624  axcontlem7  25625  cgrxfr  25705  segletr  25764  df3nandALT1  25862  andnand1  25864  nandsym1  25888  itg2addnc  25961  trer  26012  fneval  26060  neifg  26093  opropabco  26118  f1opr  26119  isdrngo1  26265  keridl  26335  ispridlc  26373  an43OLD  26389  prtlem70  26391  prtlem100  26397  prtlem15  26417  mzpcompact2lem  26501  fz1eqin  26520  rexrabdioph  26547  expdiophlem1  26785  dford4  26793  fnwe2lem2  26819  islinds2  26954  fgraphopab  27200  2sbc5g  27287  pm14.12  27292  stoweidlem26  27445  stoweidlem35  27454  reuan  27628  2reu4a  27637  dfdfat2  27666  ffnaov  27734  frgra3v  27757  4cycl2vnunb  27772  2sb5nd  27992  uun2221  28268  uun2221p1  28269  uun2221p2  28270  2sb5ndVD  28365  2sb5ndALT  28388  bnj251  28406  bnj252  28407  bnj257  28411  bnj290  28414  bnj1304  28531  bnj153  28591  bnj543  28604  bnj571  28617  bnj580  28624  bnj607  28627  bnj882  28637  bnj964  28654  bnj996  28666  bnj1033  28678  bnj1176  28714  bnj1186  28716  bnj1189  28718  bnj1204  28721  bnj1253  28726  bnj1452  28761  bnj1463  28764  sb6NEW7  28932  2sb5NEW7  28944  sbel2xNEW7  28949  2sb5rfOLD7  29080  islshpat  29134  lcvbr2  29139  lcvbr3  29140  lcvnbtwn2  29144  ellkr  29206  cvrval2  29391  cvrnbtwn2  29392  cvrnbtwn3  29393  cvrnbtwn4  29396  ishlat2  29470  lplnexatN  29679  islvol5  29695  dath  29852  pmapglb  29886  polval2N  30022  pclfinclN  30066  lhpexle3  30128  4atex2  30193  4atex2-0bOLDN  30195  isltrn2N  30236  cdleme0nex  30406  cdleme22b  30457  cdlemg17pq  30788  cdlemg19  30800  cdlemg21  30802  cdlemg33d  30825  dibopelvalN  31260  dibopelval2  31262  dib1dim  31282  dicelval2N  31299  diclspsn  31311  lcdlss  31736  mapd1o  31765
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 178  df-an 361
  Copyright terms: Public domain W3C validator