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  1837  19.41  1896  3exdistr  1929  4exdistr  1930  4exdistrOLD  1931  sb6  2148  2sb5  2161  2sb5rf  2167  sbel2x  2175  eu2  2279  eu3  2280  mo4f  2286  eu5  2292  eu4  2293  euan  2311  2mos  2333  2eu4  2337  2eu6  2339  clelab  2524  nonconne  2574  r2exf  2702  ceqsex3v  2954  ceqsex4v  2955  ceqsex8v  2957  reu2  3082  reu6  3083  reu4  3088  reu7  3089  2reu5lem3  3101  2reu5  3102  rmo3  3208  dfpss2  3392  difdif  3433  raldifb  3447  inass  3511  dfss4  3535  dfin2  3537  indi  3547  indifdir  3557  difin0ss  3654  inssdif0  3655  ssunpr  3921  unipr  3989  uniun  3994  uniin  3995  iunin2  4115  iundif2  4118  iindif2  4120  iinin2  4121  axrep1  4281  axrep4  4284  notzfaus  4334  eqvinop  4401  opcom  4410  opeqsn  4412  ordtri3or  4573  uniuni  4675  reusv2lem4  4686  tfindsg  4799  findsg  4831  fconstmpt  4880  opeliunxp  4888  xpundi  4889  elvvv  4896  xpiindi  4969  elcnv2  5009  cnvuni  5016  dmuni  5038  opelres  5110  elima3  5169  imai  5177  imainss  5246  ssrnres  5268  cnvresima  5318  mptpreima  5322  coundir  5331  rnco  5335  coass  5347  relrelss  5352  dffun2  5423  dffun3  5424  dffun4  5425  dffun5  5426  dffun6f  5427  dffun7  5438  dffun8  5439  dffun9  5440  svrelfun  5473  fncnv  5474  funcnvuni  5477  imadif  5487  dfmpt3  5526  fint  5581  fin  5582  dff12  5597  fores  5621  dff1o4  5641  eqfnfv3  5788  fndmin  5796  fniniseg  5810  rexsupp  5814  unpreima  5815  ffnfvf  5854  fsn2  5867  opabex3d  5948  opabex3  5949  dff13f  5965  isocnv2  6010  ffnov  6133  eqfnov  6135  foov  6179  difxp  6339  frxp  6415  soxp  6418  mpt2xopovel  6430  brtpos  6447  tpostpos  6458  dfsmo2  6568  tfrlem2  6596  rdglem1  6632  tz7.49  6661  brwitnlem  6710  oeeu  6805  erinxp  6937  mapsncnv  7019  cbvixp  7038  ixpin  7046  ixpiin  7047  mptelixpg  7058  elixpsn  7060  ixpsnf1o  7061  mapsnen  7143  xpassen  7161  omxpenlem  7168  sbthcl  7188  dfsup2OLD  7406  wemapso2lem  7475  dford2  7531  inf2  7534  zfinf  7550  trcl  7620  iscard2  7819  leweon  7849  aceq1  7954  dfac3  7958  dfac4  7959  dfac5lem2  7961  dfac5lem3  7962  dfac5  7965  kmlem3  7988  kmlem4  7989  kmlem14  7999  kmlem15  8000  dfackm  8002  infmap2  8054  cf0  8087  fin23lem25  8160  zorn2lem7  8338  brdom6disj  8366  zfcndrep  8445  zfcndinf  8449  fpwwe  8477  axgroth4  8663  grothprim  8665  grothtsk  8666  nqpr  8847  opelreal  8961  elnnz  10248  elznn0nn  10251  peano2uz2  10313  nnwos  10500  dflt2  10697  xmullem  10799  elfzuzb  11009  4fvwrd4  11076  fzm1  11082  elfznelfzo  11147  fzind2  11153  hashinfxadd  11614  hashfun  11655  brfi1uzind  11670  shftdm  11841  rexfiuz  12106  mertenslem2  12617  mertens  12618  divalglem10  12877  ndvdssub  12882  bitsmod  12903  algcvgblem  13023  isprm2  13042  isprm4  13044  hashdvds  13119  infpn2  13236  hashbc0  13328  xpscf  13746  funcpropd  14052  isffth2  14068  eldmcoa  14175  setcinv  14200  xpccatid  14240  yonedainv  14333  ispos  14359  ispos2  14360  istsr2  14605  spwmo  14613  isnsg2  14925  isnsg4  14938  isgim  15004  oppgid  15107  oppgcntz  15115  efgval2  15311  iscyg2  15447  dmdprdd  15515  subgdmdprd  15547  oppr1  15694  opprunit  15721  opprirred  15762  isrhm  15779  subsubrg2  15850  islmim  16089  lbsextg  16189  lidlnz  16254  isdomn2  16314  opsrtoslem1  16499  unocv  16862  pjfval2  16891  istop2g  16924  istps4OLD  16943  isbasis2g  16968  tgval2  16976  isclo2  17107  isnrm2  17376  is1stc2  17458  llyi  17490  isfbas2  17820  elfg  17856  ufinffr  17914  isfcls  17994  alexsubALTlem2  18032  alexsubALTlem3  18033  cnextcn  18051  ustfilxp  18195  iscusp2  18285  elcncf1di  18878  tchcph  19147  iscau3  19184  caucfil  19189  ellogdm  20483  dvdsflsumcom  20926  logfac2  20954  dchrelbas3  20975  dchrvmasumlema  21147  nb3grapr2  21416  uvtx01vtx  21454  3v3e3cycl2  21604  isgrpo2  21738  hhcms  22658  isch3  22697  ocsh  22738  pjhtheu  22849  pjpreeq  22853  h1deoi  23004  h1dei  23005  eleigvec  23413  cvbr2  23739  cvnbtwn2  23743  cvnbtwn4  23745  mdsl2i  23778  cvmdi  23780  mdsymlem6  23864  cdj3lem3b  23896  mo5f  23925  nmo  23926  rexunirn  23931  rmo3f  23935  rmo4fOLD  23936  rmo4f  23937  unipreima  24009  1stpreima  24048  isrnsigaOLD  24448  isrnsiga  24449  ballotlemodife  24708  erdszelem9  24838  cvmlift2lem9  24951  cvmlift2lem13  24955  axinfprim  25108  axacprim  25109  cbvprod  25194  prodmo  25215  iprodmul  25269  coep  25322  dfso2  25325  dford5reg  25352  dfon2lem5  25357  dfon2  25362  preduz  25414  wfi  25421  trpredmintr  25448  frind  25457  tfrALTlem  25490  frr3g  25494  brtxp2  25635  brpprod3a  25640  elfix  25657  dffix2  25659  dfom5b  25666  dffun10  25667  elfuns  25668  brcart  25685  brimg  25690  brsuccf  25694  funpartlem  25695  axcontlem5  25811  axcontlem6  25812  axcontlem7  25813  cgrxfr  25893  segletr  25952  df3nandALT1  26050  andnand1  26052  nandsym1  26076  cnambfre  26154  itg2addnc  26158  trer  26209  fneval  26257  neifg  26290  opropabco  26315  f1opr  26316  isdrngo1  26462  keridl  26532  ispridlc  26570  an43OLD  26586  prtlem70  26588  prtlem100  26594  prtlem15  26614  mzpcompact2lem  26698  fz1eqin  26717  rexrabdioph  26744  expdiophlem1  26982  dford4  26990  fnwe2lem2  27016  islinds2  27151  fgraphopab  27397  2sbc5g  27484  pm14.12  27489  stoweidlem26  27642  stoweidlem35  27651  reuan  27825  2reu4a  27834  dfdfat2  27862  ffnaov  27930  rexdifpr  27947  dff14a  27959  dff14b  27960  usg2spthonot0  28086  frgra3v  28106  4cycl2vnunb  28121  usg2spot2nb  28168  2sb5nd  28358  uun2221  28634  uun2221p1  28635  uun2221p2  28636  2sb5ndVD  28731  2sb5ndALT  28754  bnj251  28772  bnj252  28773  bnj257  28777  bnj290  28780  bnj1304  28897  bnj153  28957  bnj543  28970  bnj571  28983  bnj580  28990  bnj607  28993  bnj882  29003  bnj964  29020  bnj996  29032  bnj1033  29044  bnj1176  29080  bnj1186  29082  bnj1189  29084  bnj1204  29087  bnj1253  29092  bnj1452  29127  bnj1463  29130  sb6NEW7  29298  2sb5NEW7  29310  sbel2xNEW7  29315  2sb5rfOLD7  29446  islshpat  29500  lcvbr2  29505  lcvbr3  29506  lcvnbtwn2  29510  ellkr  29572  cvrval2  29757  cvrnbtwn2  29758  cvrnbtwn3  29759  cvrnbtwn4  29762  ishlat2  29836  lplnexatN  30045  islvol5  30061  dath  30218  pmapglb  30252  polval2N  30388  pclfinclN  30432  lhpexle3  30494  4atex2  30559  4atex2-0bOLDN  30561  isltrn2N  30602  cdleme0nex  30772  cdleme22b  30823  cdlemg17pq  31154  cdlemg19  31166  cdlemg21  31168  cdlemg33d  31191  dibopelvalN  31626  dibopelval2  31628  dib1dim  31648  dicelval2N  31665  diclspsn  31677  lcdlss  32102  mapd1o  32131
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