MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anbi2i Structured version   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  1300  cadan  1401  cadcoma  1404  nic-mpALT  1446  nic-axALT  1448  19.35  1610  19.27  1841  19.41  1900  3exdistr  1933  4exdistr  1934  4exdistrOLD  1935  sbn  2117  sb6  2174  2sb5  2187  2sb5rf  2193  sbel2x  2201  eu2  2305  eu3  2306  mo4f  2312  eu5  2318  eu4  2319  euan  2337  2mos  2359  2eu4  2363  2eu6  2365  clelab  2555  nonconne  2605  r2exf  2733  ceqsex3v  2986  ceqsex4v  2987  ceqsex8v  2989  reu2  3114  reu6  3115  reu4  3120  reu7  3121  2reu5lem3  3133  2reu5  3134  rmo3  3240  dfpss2  3424  difdif  3465  raldifb  3479  inass  3543  dfss4  3567  dfin2  3569  indi  3579  indifdir  3589  difin0ss  3686  inssdif0  3687  ssunpr  3953  unipr  4021  uniun  4026  uniin  4027  iunin2  4147  iundif2  4150  iindif2  4152  iinin2  4153  axrep1  4313  axrep4  4316  notzfaus  4366  eqvinop  4433  opcom  4442  opeqsn  4444  ordtri3or  4605  uniuni  4708  reusv2lem4  4719  tfindsg  4832  findsg  4864  fconstmpt  4913  opeliunxp  4921  xpundi  4922  elvvv  4929  xpiindi  5002  elcnv2  5042  cnvuni  5049  dmuni  5071  opelres  5143  elima3  5202  imai  5210  imainss  5279  ssrnres  5301  cnvresima  5351  mptpreima  5355  coundir  5364  rnco  5368  coass  5380  relrelss  5385  dffun2  5456  dffun3  5457  dffun4  5458  dffun5  5459  dffun6f  5460  dffun7  5471  dffun8  5472  dffun9  5473  svrelfun  5506  fncnv  5507  funcnvuni  5510  imadif  5520  dfmpt3  5559  fint  5614  fin  5615  dff12  5630  fores  5654  dff1o4  5674  eqfnfv3  5821  fndmin  5829  fniniseg  5843  rexsupp  5847  unpreima  5848  ffnfvf  5887  fsn2  5900  opabex3d  5981  opabex3  5982  dff13f  5998  isocnv2  6043  ffnov  6166  eqfnov  6168  foov  6212  difxp  6372  frxp  6448  soxp  6451  mpt2xopovel  6463  brtpos  6480  tpostpos  6491  dfsmo2  6601  tfrlem2  6629  rdglem1  6665  tz7.49  6694  brwitnlem  6743  oeeu  6838  erinxp  6970  mapsncnv  7052  cbvixp  7071  ixpin  7079  ixpiin  7080  mptelixpg  7091  elixpsn  7093  ixpsnf1o  7094  mapsnen  7176  xpassen  7194  omxpenlem  7201  sbthcl  7221  dfsup2OLD  7440  wemapso2lem  7511  dford2  7567  inf2  7570  zfinf  7586  trcl  7656  iscard2  7855  leweon  7885  aceq1  7990  dfac3  7994  dfac4  7995  dfac5lem2  7997  dfac5lem3  7998  dfac5  8001  kmlem3  8024  kmlem4  8025  kmlem14  8035  kmlem15  8036  dfackm  8038  infmap2  8090  cf0  8123  fin23lem25  8196  zorn2lem7  8374  brdom6disj  8402  zfcndrep  8481  zfcndinf  8485  fpwwe  8513  axgroth4  8699  grothprim  8701  grothtsk  8702  nqpr  8883  opelreal  8997  elnnz  10284  elznn0nn  10287  peano2uz2  10349  nnwos  10536  dflt2  10733  xmullem  10835  elfzuzb  11045  4fvwrd4  11113  fzm1  11119  elfznelfzo  11184  fzind2  11190  hashinfxadd  11651  hashfun  11692  brfi1uzind  11707  shftdm  11878  rexfiuz  12143  mertenslem2  12654  mertens  12655  divalglem10  12914  ndvdssub  12919  bitsmod  12940  algcvgblem  13060  isprm2  13079  isprm4  13081  hashdvds  13156  infpn2  13273  hashbc0  13365  xpscf  13783  funcpropd  14089  isffth2  14105  eldmcoa  14212  setcinv  14237  xpccatid  14277  yonedainv  14370  ispos  14396  ispos2  14397  istsr2  14642  spwmo  14650  isnsg2  14962  isnsg4  14975  isgim  15041  oppgid  15144  oppgcntz  15152  efgval2  15348  iscyg2  15484  dmdprdd  15552  subgdmdprd  15584  oppr1  15731  opprunit  15758  opprirred  15799  isrhm  15816  subsubrg2  15887  islmim  16126  lbsextg  16226  lidlnz  16291  isdomn2  16351  opsrtoslem1  16536  unocv  16899  pjfval2  16928  istop2g  16961  istps4OLD  16980  isbasis2g  17005  tgval2  17013  isclo2  17144  isnrm2  17414  is1stc2  17497  llyi  17529  isfbas2  17859  elfg  17895  ufinffr  17953  isfcls  18033  alexsubALTlem2  18071  alexsubALTlem3  18072  cnextcn  18090  ustfilxp  18234  iscusp2  18324  elcncf1di  18917  tchcph  19186  iscau3  19223  caucfil  19228  ellogdm  20522  dvdsflsumcom  20965  logfac2  20993  dchrelbas3  21014  dchrvmasumlema  21186  nb3grapr2  21455  uvtx01vtx  21493  3v3e3cycl2  21643  isgrpo2  21777  hhcms  22697  isch3  22736  ocsh  22777  pjhtheu  22888  pjpreeq  22892  h1deoi  23043  h1dei  23044  eleigvec  23452  cvbr2  23778  cvnbtwn2  23782  cvnbtwn4  23784  mdsl2i  23817  cvmdi  23819  mdsymlem6  23903  cdj3lem3b  23935  mo5f  23964  nmo  23965  rexunirn  23970  rmo3f  23974  rmo4fOLD  23975  rmo4f  23976  unipreima  24048  1stpreima  24087  isrnsigaOLD  24487  isrnsiga  24488  ballotlemodife  24747  erdszelem9  24877  cvmlift2lem9  24990  cvmlift2lem13  24994  axinfprim  25147  axacprim  25148  cbvprod  25233  prodmo  25254  iprodmul  25308  coep  25366  dfso2  25369  dford5reg  25401  dfon2lem5  25406  dfon2  25411  preduz  25467  wfi  25474  trpredmintr  25501  frind  25510  frr3g  25573  brtxp2  25718  brpprod3a  25723  dfom5b  25749  brcart  25769  brimg  25774  brsuccf  25778  funpartlem  25779  axcontlem5  25899  axcontlem6  25900  axcontlem7  25901  cgrxfr  25981  segletr  26040  df3nandALT1  26138  andnand1  26140  nandsym1  26164  cnambfre  26245  itg2addnc  26249  ftc1anc  26278  trer  26310  fneval  26358  neifg  26391  opropabco  26416  f1opr  26417  isdrngo1  26563  keridl  26633  ispridlc  26671  an43OLD  26687  prtlem70  26689  prtlem100  26695  prtlem15  26715  mzpcompact2lem  26799  fz1eqin  26818  rexrabdioph  26845  expdiophlem1  27083  dford4  27091  fnwe2lem2  27117  islinds2  27251  fgraphopab  27497  2sbc5g  27584  pm14.12  27589  stoweidlem26  27742  stoweidlem35  27751  reuan  27925  2reu4a  27934  dfdfat2  27962  ffnaov  28030  rexdifpr  28049  dff14a  28064  dff14b  28065  usg2spthonot0  28309  frgra3v  28329  4cycl2vnunb  28344  usg2spot2nb  28391  2sb5nd  28584  uun2221  28862  uun2221p1  28863  uun2221p2  28864  2sb5ndVD  28959  2sb5ndALT  28981  bnj251  29003  bnj252  29004  bnj257  29008  bnj290  29011  bnj1304  29128  bnj153  29188  bnj543  29201  bnj571  29214  bnj580  29221  bnj607  29224  bnj882  29234  bnj964  29251  bnj996  29263  bnj1033  29275  bnj1176  29311  bnj1186  29313  bnj1189  29315  bnj1204  29318  bnj1253  29323  bnj1452  29358  bnj1463  29361  sb6NEW7  29534  2sb5NEW7  29546  sbel2xNEW7  29551  2sb5rfOLD7  29698  islshpat  29752  lcvbr2  29757  lcvbr3  29758  lcvnbtwn2  29762  ellkr  29824  cvrval2  30009  cvrnbtwn2  30010  cvrnbtwn3  30011  cvrnbtwn4  30014  ishlat2  30088  lplnexatN  30297  islvol5  30313  dath  30470  pmapglb  30504  polval2N  30640  pclfinclN  30684  lhpexle3  30746  4atex2  30811  4atex2-0bOLDN  30813  isltrn2N  30854  cdleme0nex  31024  cdleme22b  31075  cdlemg17pq  31406  cdlemg19  31418  cdlemg21  31420  cdlemg33d  31443  dibopelvalN  31878  dibopelval2  31880  dib1dim  31900  dicelval2N  31917  diclspsn  31929  lcdlss  32354  mapd1o  32383
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