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

Theorem anbi2i 675
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 10 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
32pm5.32i 618 1  |-  ( ( ch  /\  ph )  <->  ( ch  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  anbi12i  678  an4  797  an42  798  anandir  802  dfbi3  863  dn1  932  nannan  1291  cadan  1382  cadcoma  1385  nic-mpALT  1427  nic-axALT  1429  19.35  1587  19.27  1805  3exdistr  1851  4exdistr  1852  sb6  2038  2sb5  2051  2sb5rf  2056  sbel2x  2064  eu2  2168  eu3  2169  mo4f  2175  eu5  2181  eu4  2182  euan  2200  2mos  2222  2eu4  2226  2eu6  2228  clelab  2403  nonconne  2453  r2exf  2579  ceqsex3v  2826  ceqsex4v  2827  ceqsex8v  2829  reu2  2953  reu6  2954  reu4  2959  reu7  2960  2reu5lem3  2972  2reu5  2973  rmo3  3078  dfpss2  3261  difdif  3302  inass  3379  dfss4  3403  dfin2  3405  indi  3415  indifdir  3425  difin0ss  3520  inssdif0  3521  ssunpr  3776  unipr  3841  uniun  3846  uniin  3847  iunin2  3966  iundif2  3969  iindif2  3971  iinin2  3972  axrep1  4132  axrep4  4135  notzfaus  4185  eqvinop  4251  opcom  4260  opeqsn  4262  ordtri3or  4424  trsuc2OLD  4477  uniuni  4527  reusv2lem4  4538  tfindsg  4651  findsg  4683  fconstmpt  4732  opeliunxp  4740  xpundi  4741  elvvv  4749  xpiindi  4821  elcnv2  4859  cnvuni  4866  dmuni  4888  opelres  4960  elima3  5019  imai  5027  imainss  5096  ssrnres  5116  cnvresima  5162  mptpreima  5166  coundir  5175  rnco  5179  coass  5191  relrelss  5196  dffun2  5265  dffun3  5266  dffun4  5267  dffun5  5268  dffun6f  5269  dffun7  5280  dffun8  5281  dffun9  5282  svrelfun  5313  fncnv  5314  funcnvuni  5317  imadif  5327  dfmpt3  5366  fint  5420  fin  5421  dff12  5436  fores  5460  dff1o4  5480  eqfnfv3  5624  fndmin  5632  fniniseg  5646  rexsupp  5650  unpreima  5651  ffnfvf  5686  fsn2  5698  opabex3  5769  dff13f  5784  isocnv2  5828  ffnov  5948  eqfnov  5950  foov  5994  difxp  6153  frxp  6225  soxp  6228  brtpos  6243  tpostpos  6254  dfsmo2  6364  tfrlem2  6392  rdglem1  6428  tz7.49  6457  brwitnlem  6506  oeeu  6601  erinxp  6733  mapsncnv  6814  cbvixp  6833  ixpin  6841  ixpiin  6842  mptelixpg  6853  elixpsn  6855  ixpsnf1o  6856  mapsnen  6938  xpassen  6956  omxpenlem  6963  sbthcl  6983  dfsup2OLD  7196  wemapso2lem  7265  dford2  7321  inf2  7324  zfinf  7340  trcl  7410  iscard2  7609  leweon  7639  aceq1  7744  dfac3  7748  dfac4  7749  dfac5lem2  7751  dfac5lem3  7752  dfac5  7755  kmlem3  7778  kmlem4  7779  kmlem14  7789  kmlem15  7790  dfackm  7792  infmap2  7844  cf0  7877  fin23lem25  7950  zorn2lem7  8129  brdom6disj  8157  zfcndrep  8236  zfcndinf  8240  fpwwe  8268  axgroth4  8454  grothprim  8456  grothtsk  8457  nqpr  8638  opelreal  8752  elnnz  10034  elznn0nn  10037  peano2uz2  10099  nnwos  10286  dflt2  10482  xmullem  10584  elfzuzb  10792  fzm1  10862  fzind2  10923  hashfun  11389  shftdm  11566  rexfiuz  11831  mertenslem2  12341  mertens  12342  divalglem10  12601  ndvdssub  12606  bitsmod  12627  algcvgblem  12747  isprm2  12766  isprm4  12768  hashdvds  12843  infpn2  12960  hashbc0  13052  xpscf  13468  funcpropd  13774  isffth2  13790  eldmcoa  13897  setcinv  13922  xpccatid  13962  yonedainv  14055  ispos  14081  ispos2  14082  istsr2  14327  spwmo  14335  isnsg2  14647  isnsg4  14660  isgim  14726  oppgid  14829  oppgcntz  14837  efgval2  15033  iscyg2  15169  dmdprdd  15237  subgdmdprd  15269  oppr1  15416  opprunit  15443  opprirred  15484  isrhm  15501  subsubrg2  15572  islmim  15815  lbsextg  15915  lidlnz  15980  isdomn2  16040  opsrtoslem1  16225  unocv  16580  pjfval2  16609  istop2g  16642  istps4OLD  16661  isbasis2g  16686  tgval2  16694  isclo2  16825  isnrm2  17086  is1stc2  17168  llyi  17200  isfbas2  17530  elfg  17566  ufinffr  17624  isfcls  17704  alexsubALTlem2  17742  alexsubALTlem3  17743  elcncf1di  18399  tchcph  18667  iscau3  18704  caucfil  18709  ellogdm  19986  dvdsflsumcom  20428  logfac2  20456  dchrelbas3  20477  dchrvmasumlema  20649  isgrpo2  20864  hhcms  21782  isch3  21821  ocsh  21862  pjhtheu  21973  pjpreeq  21977  h1deoi  22128  h1dei  22129  eleigvec  22537  cvbr2  22863  cvnbtwn2  22867  cvnbtwn4  22869  mdsl2i  22902  cvmdi  22904  mdsymlem6  22988  cdj3lem3b  23020  ballotlemodife  23056  rexunirn  23140  mo5f  23143  nmo  23144  rmo3f  23178  rmo4fOLD  23179  rmo4f  23180  unipreima  23209  isrnsigaOLD  23473  isrnsiga  23474  isibfm  23593  erdszelem9  23730  cvmlift2lem9  23842  cvmlift2lem13  23846  axinfprim  24052  axacprim  24053  coep  24108  dfso2  24111  dford5reg  24138  dfon2lem5  24143  dfon2  24148  preduz  24200  wfi  24207  trpredmintr  24234  frind  24243  tfrALTlem  24276  frr3g  24280  brtxp2  24421  brpprod3a  24426  elfix  24443  dffix2  24445  dfom5b  24452  dffun10  24453  elfuns  24454  brcart  24471  brimg  24476  brsuccf  24480  axcontlem5  24596  axcontlem6  24597  axcontlem7  24598  cgrxfr  24678  segletr  24737  df3nandALT1  24835  andnand1  24837  nandsym1  24861  and4com  24940  eqvinopb  24965  dfdir2  25291  cbvprodi  25312  vecval1b  25451  bisig0  26062  isconcl5a  26101  isconcl5ab  26102  isibcg  26191  cnvresimaOLD  26226  trer  26227  fneval  26287  neifg  26320  opropabco  26389  f1opr  26391  isdrngo1  26587  keridl  26657  ispridlc  26695  an43OLD  26713  prtlem70  26715  prtlem100  26721  prtlem15  26743  mzpcompact2lem  26829  fz1eqin  26848  rexrabdioph  26875  expdiophlem1  27114  dford4  27122  fnwe2lem2  27148  islinds2  27283  fgraphopab  27529  2sbc5g  27616  pm14.12  27621  stoweidlem26  27775  stoweidlem35  27784  reuan  27958  2reu4a  27967  dfdfat2  27994  ffnaov  28059  mpt2xopovel  28086  uvtx01vtx  28164  frgra3v  28180  2sb5nd  28326  uun2221  28588  uun2221p1  28589  uun2221p2  28590  2sb5ndVD  28686  2sb5ndALT  28709  bnj251  28727  bnj252  28728  bnj257  28732  bnj290  28735  bnj1304  28852  bnj153  28912  bnj543  28925  bnj571  28938  bnj580  28945  bnj607  28948  bnj882  28958  bnj964  28975  bnj996  28987  bnj1033  28999  bnj1176  29035  bnj1186  29037  bnj1189  29039  bnj1204  29042  bnj1253  29047  bnj1452  29082  bnj1463  29085  islshpat  29207  lcvbr2  29212  lcvbr3  29213  lcvnbtwn2  29217  ellkr  29279  cvrval2  29464  cvrnbtwn2  29465  cvrnbtwn3  29466  cvrnbtwn4  29469  ishlat2  29543  lplnexatN  29752  islvol5  29768  dath  29925  pmapglb  29959  polval2N  30095  pclfinclN  30139  lhpexle3  30201  4atex2  30266  4atex2-0bOLDN  30268  isltrn2N  30309  cdleme0nex  30479  cdleme22b  30530  cdlemg17pq  30861  cdlemg19  30873  cdlemg21  30875  cdlemg33d  30898  dibopelvalN  31333  dibopelval2  31335  dib1dim  31355  dicelval2N  31372  diclspsn  31384  lcdlss  31809  mapd1o  31838
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