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  1590  19.27  1817  3exdistr  1863  4exdistr  1864  sb6  2051  2sb5  2064  2sb5rf  2069  sbel2x  2077  eu2  2181  eu3  2182  mo4f  2188  eu5  2194  eu4  2195  euan  2213  2mos  2235  2eu4  2239  2eu6  2241  clelab  2416  nonconne  2466  r2exf  2592  ceqsex3v  2839  ceqsex4v  2840  ceqsex8v  2842  reu2  2966  reu6  2967  reu4  2972  reu7  2973  2reu5lem3  2985  2reu5  2986  rmo3  3091  dfpss2  3274  difdif  3315  inass  3392  dfss4  3416  dfin2  3418  indi  3428  indifdir  3438  difin0ss  3533  inssdif0  3534  ssunpr  3792  unipr  3857  uniun  3862  uniin  3863  iunin2  3982  iundif2  3985  iindif2  3987  iinin2  3988  axrep1  4148  axrep4  4151  notzfaus  4201  eqvinop  4267  opcom  4276  opeqsn  4278  ordtri3or  4440  trsuc2OLD  4493  uniuni  4543  reusv2lem4  4554  tfindsg  4667  findsg  4699  fconstmpt  4748  opeliunxp  4756  xpundi  4757  elvvv  4765  xpiindi  4837  elcnv2  4875  cnvuni  4882  dmuni  4904  opelres  4976  elima3  5035  imai  5043  imainss  5112  ssrnres  5132  cnvresima  5178  mptpreima  5182  coundir  5191  rnco  5195  coass  5207  relrelss  5212  dffun2  5281  dffun3  5282  dffun4  5283  dffun5  5284  dffun6f  5285  dffun7  5296  dffun8  5297  dffun9  5298  svrelfun  5329  fncnv  5330  funcnvuni  5333  imadif  5343  dfmpt3  5382  fint  5436  fin  5437  dff12  5452  fores  5476  dff1o4  5496  eqfnfv3  5640  fndmin  5648  fniniseg  5662  rexsupp  5666  unpreima  5667  ffnfvf  5702  fsn2  5714  opabex3  5785  dff13f  5800  isocnv2  5844  ffnov  5964  eqfnov  5966  foov  6010  difxp  6169  frxp  6241  soxp  6244  brtpos  6259  tpostpos  6270  dfsmo2  6380  tfrlem2  6408  rdglem1  6444  tz7.49  6473  brwitnlem  6522  oeeu  6617  erinxp  6749  mapsncnv  6830  cbvixp  6849  ixpin  6857  ixpiin  6858  mptelixpg  6869  elixpsn  6871  ixpsnf1o  6872  mapsnen  6954  xpassen  6972  omxpenlem  6979  sbthcl  6999  dfsup2OLD  7212  wemapso2lem  7281  dford2  7337  inf2  7340  zfinf  7356  trcl  7426  iscard2  7625  leweon  7655  aceq1  7760  dfac3  7764  dfac4  7765  dfac5lem2  7767  dfac5lem3  7768  dfac5  7771  kmlem3  7794  kmlem4  7795  kmlem14  7805  kmlem15  7806  dfackm  7808  infmap2  7860  cf0  7893  fin23lem25  7966  zorn2lem7  8145  brdom6disj  8173  zfcndrep  8252  zfcndinf  8256  fpwwe  8284  axgroth4  8470  grothprim  8472  grothtsk  8473  nqpr  8654  opelreal  8768  elnnz  10050  elznn0nn  10053  peano2uz2  10115  nnwos  10302  dflt2  10498  xmullem  10600  elfzuzb  10808  fzm1  10878  fzind2  10939  hashfun  11405  shftdm  11582  rexfiuz  11847  mertenslem2  12357  mertens  12358  divalglem10  12617  ndvdssub  12622  bitsmod  12643  algcvgblem  12763  isprm2  12782  isprm4  12784  hashdvds  12859  infpn2  12976  hashbc0  13068  xpscf  13484  funcpropd  13790  isffth2  13806  eldmcoa  13913  setcinv  13938  xpccatid  13978  yonedainv  14071  ispos  14097  ispos2  14098  istsr2  14343  spwmo  14351  isnsg2  14663  isnsg4  14676  isgim  14742  oppgid  14845  oppgcntz  14853  efgval2  15049  iscyg2  15185  dmdprdd  15253  subgdmdprd  15285  oppr1  15432  opprunit  15459  opprirred  15500  isrhm  15517  subsubrg2  15588  islmim  15831  lbsextg  15931  lidlnz  15996  isdomn2  16056  opsrtoslem1  16241  unocv  16596  pjfval2  16625  istop2g  16658  istps4OLD  16677  isbasis2g  16702  tgval2  16710  isclo2  16841  isnrm2  17102  is1stc2  17184  llyi  17216  isfbas2  17546  elfg  17582  ufinffr  17640  isfcls  17720  alexsubALTlem2  17758  alexsubALTlem3  17759  elcncf1di  18415  tchcph  18683  iscau3  18720  caucfil  18725  ellogdm  20002  dvdsflsumcom  20444  logfac2  20472  dchrelbas3  20493  dchrvmasumlema  20665  isgrpo2  20880  hhcms  21798  isch3  21837  ocsh  21878  pjhtheu  21989  pjpreeq  21993  h1deoi  22144  h1dei  22145  eleigvec  22553  cvbr2  22879  cvnbtwn2  22883  cvnbtwn4  22885  mdsl2i  22918  cvmdi  22920  mdsymlem6  23004  cdj3lem3b  23036  ballotlemodife  23072  rexunirn  23156  mo5f  23159  nmo  23160  rmo3f  23194  rmo4fOLD  23195  rmo4f  23196  unipreima  23224  isrnsigaOLD  23488  isrnsiga  23489  isibfm  23608  erdszelem9  23745  cvmlift2lem9  23857  cvmlift2lem13  23861  axinfprim  24067  axacprim  24068  cbvcprod  24137  prodmo  24159  coep  24178  dfso2  24181  dford5reg  24208  dfon2lem5  24213  dfon2  24218  preduz  24270  wfi  24277  trpredmintr  24304  frind  24313  tfrALTlem  24346  frr3g  24350  brtxp2  24491  brpprod3a  24496  elfix  24513  dffix2  24515  dfom5b  24522  dffun10  24523  elfuns  24524  brcart  24541  brimg  24546  brsuccf  24550  funpartlem  24551  axcontlem5  24667  axcontlem6  24668  axcontlem7  24669  cgrxfr  24749  segletr  24808  df3nandALT1  24906  andnand1  24908  nandsym1  24932  itg2addnc  25004  and4com  25042  eqvinopb  25067  dfdir2  25393  cbvprodi  25414  vecval1b  25553  bisig0  26164  isconcl5a  26203  isconcl5ab  26204  isibcg  26293  cnvresimaOLD  26328  trer  26329  fneval  26389  neifg  26422  opropabco  26491  f1opr  26493  isdrngo1  26689  keridl  26759  ispridlc  26797  an43OLD  26815  prtlem70  26817  prtlem100  26823  prtlem15  26845  mzpcompact2lem  26931  fz1eqin  26950  rexrabdioph  26977  expdiophlem1  27216  dford4  27224  fnwe2lem2  27250  islinds2  27385  fgraphopab  27631  2sbc5g  27718  pm14.12  27723  stoweidlem26  27877  stoweidlem35  27886  reuan  28060  2reu4a  28069  dfdfat2  28098  ffnaov  28166  opabex3d  28189  mpt2xopovel  28201  elfznelfzo  28212  4fvwrd4  28219  nb3grapr2  28289  uvtx01vtx  28304  3v3e3cycl2  28409  frgra3v  28425  4cycl2vnunb  28438  2sb5nd  28624  uun2221  28901  uun2221p1  28902  uun2221p2  28903  2sb5ndVD  29001  2sb5ndALT  29024  bnj251  29042  bnj252  29043  bnj257  29047  bnj290  29050  bnj1304  29167  bnj153  29227  bnj543  29240  bnj571  29253  bnj580  29260  bnj607  29263  bnj882  29273  bnj964  29290  bnj996  29302  bnj1033  29314  bnj1176  29350  bnj1186  29352  bnj1189  29354  bnj1204  29357  bnj1253  29362  bnj1452  29397  bnj1463  29400  sb6NEW7  29568  2sb5NEW7  29580  sbel2xNEW7  29585  2sb5rfOLD7  29717  islshpat  29829  lcvbr2  29834  lcvbr3  29835  lcvnbtwn2  29839  ellkr  29901  cvrval2  30086  cvrnbtwn2  30087  cvrnbtwn3  30088  cvrnbtwn4  30091  ishlat2  30165  lplnexatN  30374  islvol5  30390  dath  30547  pmapglb  30581  polval2N  30717  pclfinclN  30761  lhpexle3  30823  4atex2  30888  4atex2-0bOLDN  30890  isltrn2N  30931  cdleme0nex  31101  cdleme22b  31152  cdlemg17pq  31483  cdlemg19  31495  cdlemg21  31497  cdlemg33d  31520  dibopelvalN  31955  dibopelval2  31957  dib1dim  31977  dicelval2N  31994  diclspsn  32006  lcdlss  32431  mapd1o  32460
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