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

Theorem anbi12i 697
Description: Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993.)
Hypotheses
Ref Expression
anbi12.1
anbi12.2
Assertion
Ref Expression
anbi12i

Proof of Theorem anbi12i
StepHypRef Expression
1 anbi12.1 . . 3
21anbi1i 695 . 2
3 anbi12.2 . . 3
43anbi2i 694 . 2
52, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  anbi12ci  698  ordi  864  ordir  865  orddi  869  pm5.17  888  xor  891  3anbi123i  1185  an6  1308  nanbi  1352  nanbiOLD  1353  cadan  1459  nic-axALT  1507  19.43OLD  1694  sbequ8  1744  sbbi  2142  sbnf2  2183  2mo2  2372  2eu1OLD  2377  2eu4  2380  2eu4OLD  2381  2eu6OLD  2384  sbabel  2650  sbabelOLD  2651  neanior  2782  rexeqbii  2972  r19.26m  2987  reean  3024  2ralor  3027  reu5  3073  reu2  3287  reu3  3289  2reu5lem3  3307  eqss  3518  unss  3677  ralunb  3684  ssin  3719  undi  3744  indifdir  3753  undif3  3758  inab  3765  difab  3766  reuss2  3777  reupick  3781  prss  4184  sstp  4194  tpss  4195  prsspwOLD  4203  prneimg  4211  prnebg  4212  uniin  4269  intun  4319  intpr  4320  disjiun  4442  disjxiun  4449  brin  4501  brdif  4502  ssext  4707  pweqb  4709  opthg2  4729  copsex4g  4741  eqopab2b  4782  pwin  4789  pofun  4821  wetrep  4877  elxp3  5055  soinxp  5069  weinxp  5072  csbxp  5086  relun  5124  inopab  5138  difopab  5139  inxp  5140  opelco2g  5175  cnvco  5193  dmin  5215  intasym  5387  asymref  5388  asymref2  5389  cnvdif  5417  xpnz  5431  difxp  5436  xpdifid  5440  xp11  5447  dfco2  5511  relssdmrn  5533  cnvpo  5550  cnvso  5551  xpco  5552  dffun4  5605  funun  5635  fun11  5658  fununi  5659  imadif  5668  fnres  5702  fnopabg  5709  fun  5753  fin  5770  dff1o2  5826  brprcneu  5864  dffv2  5946  fsn  6069  f13dfv  6180  dff1o6  6181  isotr  6232  eqoprab2b  6355  porpss  6584  sucelon  6652  elxp6  6832  dfoprab3  6856  opiota  6859  fsplit  6905  poxp  6912  soxp  6913  suppvalbr  6922  brtpos2  6980  tfrlem7  7071  dfer2  7331  eqer  7363  iiner  7402  uniinqs  7410  brecop  7423  eroveu  7425  erovlem  7426  mapval2  7468  ixpin  7514  boxriin  7531  brsdom  7558  xpcomco  7627  xpassen  7631  sbthlem9  7655  sbthlem10  7656  brsdom2  7661  ssenen  7711  unfi  7807  dffi3  7911  dfsup2  7922  dfsup2OLD  7923  axinf2  8078  zfinf2  8080  oemapso  8122  scottexs  8326  scott0s  8327  kardex  8333  karden  8334  dfac5lem1  8525  dfac5lem3  8527  kmlem15  8565  enfin2i  8722  fin23lem34  8747  brdom7disj  8930  fpwwe2lem12  9040  fpwwe2lem13  9041  axgroth5  9223  grothprim  9233  addsrpr  9473  mulsrpr  9474  mulgt0sr  9503  addcnsr  9533  mulcnsr  9534  ltresr  9538  axcnre  9562  1re  9616  ssxr  9675  infmsup  10546  infmrgelb  10548  infmrlb  10549  nnwos  11178  zmin  11207  xrnemnf  11357  xrnepnf  11358  xmullem  11485  xmulcom  11487  xmulneg1  11490  xmulf  11493  xrinfmss2  11531  elfzuzb  11711  fzass4  11750  seqof  12164  hashbclem  12501  hashfacen  12503  rexanre  13179  caubnd  13191  o1lo1  13360  rpnnen2  13959  isprm3  14226  prmreclem2  14435  4sqlem12  14474  isffth2  15285  fucinv  15342  lublecllem  15618  oduglb  15769  odulub  15771  issubm  15978  issubmd  15980  isnsg2  16231  oppgid  16391  symgfixf1  16462  pmtrrn2  16485  lsmdisjr  16702  lsmhash  16723  dprd0  17078  issrg  17159  dvdsrtr  17301  isirred2  17350  lss1d  17609  lspsolvlem  17788  lbsextlem2  17805  evlsval  18188  unocv  18711  iunocv  18712  gsumcom3  18901  mpt2matmul  18948  cpmidpmat  19374  tgval2  19457  fctop  19505  cctop  19507  ppttop  19508  epttop  19510  cnnei  19783  2ndcctbss  19956  txuni2  20066  txbas  20068  ptbasin  20078  txdis1cn  20136  xkococnlem  20160  opnfbas  20343  fgcl  20379  fbasrn  20385  filuni  20386  cfinfil  20394  csdfil  20395  fin1aufil  20433  rnelfmlem  20453  fmfnfmlem3  20457  txflf  20507  xmeterval  20935  reconn  21333  iimulcl  21437  iscau3  21717  rrxmvallem  21831  minveclem3  21844  pmltpc  21862  ovolfcl  21878  ismbl  21937  dyaddisj  22005  iblre  22200  plyun0  22594  logfaclbnd  23497  lgslem3  23573  lgsdir2lem5  23602  nb3grapr2  24454  cusgra3v  24464  4cycl4v4e  24666  4cycl4dv4e  24668  wlknwwlkninj  24711  wlkiswwlkinj  24718  wwlknndef  24737  clwwlknndef  24773  clwwlkf1  24796  frisusgranb  24997  frgra3v  25002  elghomOLD  25365  ajfval  25724  issh  26125  chcon2i  26382  chcon3i  26384  spanuni  26462  5oalem7  26578  3oalem3  26582  pjin2i  27112  pjin3i  27113  cvnbtwn4  27208  mdslj1i  27238  mdslj2i  27239  mdslmd1i  27248  chrelat4i  27292  chirredi  27313  cdj3i  27360  iuninc  27428  fcoinvbr  27461  suppss2f  27477  fmptdF  27495  mptfnf  27499  disjdsct  27521  cnvoprab  27546  f1od2  27547  tosglblem  27657  ordtconlem1  27906  esumpfinvalf  28082  measiuns  28188  eulerpartlemt0  28308  eulerpartlemr  28313  eulerpartlemn  28320  ballotlem2  28427  ballotlemodife  28436  derangenlem  28615  pconcon  28676  elmpst  28896  dftr6  29179  dffr5  29182  dfpo2  29184  fundmpss  29196  elpotr  29213  soseq  29334  wfrlem5  29347  wfrlem11  29353  frrlem5  29391  frrlem5c  29393  nocvxmin  29451  brtxp  29530  brpprod  29535  brsset  29539  idsset  29540  dfon3  29542  ellimits  29560  dffun10  29564  elfuns  29565  brcart  29582  brimg  29587  brapply  29588  brcap  29590  brsuccf  29591  funpartfun  29593  dfrdg4  29600  tfrqfree  29601  altopthc  29621  altopthd  29622  altopelaltxp  29626  outsideoftr  29779  df3nandALT1  29862  imnand2  29865  ismblfin  30055  mbfposadd  30062  trer  30134  gtinf  30137  neibastop1  30177  neifg  30189  inixp  30219  keridl  30429  smprngopr  30449  sbcani  30510  prtlem10  30606  prter1  30620  mzpclall  30659  mzpincl  30666  mzpindd  30678  2nn0ind  30881  dford4  30971  wopprc  30972  islmodfg  31015  isdomn3  31164  lcmcllem  31202  nzin  31223  ellimcabssub0  31623  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  2reu5a  32182  2reu1  32191  2reu4a  32194  usgpredgvALT  32400  issubmgm  32477  rabsubmgmd  32479  2zlidl  32740  mndpsuppss  32964  islininds2  33085  zlmodzxzldeplem3  33103  alsi-no-surprise  33211  onfrALTlem5  33314  onfrALTlem4  33315  undif3VD  33682  onfrALTlem5VD  33685  onfrALTlem4VD  33686  bnj887  33823  bnj976  33836  bnj1385  33891  bnj153  33938  bnj543  33951  bnj607  33974  bnj882  33984  bnj916  33991  bnj983  34009  bj-eldiag2  34607  lcvbr3  34748  isopos  34905  llnexatN  35245  snatpsubN  35474  pclclN  35615  pclfinN  35624  lhpocnel2  35743  cdlemk19w  36698  dih1dimatlem  37056  bj-ifim123g  37706  bj-ifidg  37707  bj-ifid1g  37708  bj-ifim1g  37714  bj-ifimimb  37715  bj-ifnot23  37718  bj-if1bi  37720  bj-ifbibib  37721  bj-ifor123g  37725  bj-ifororb  37726  bj-ifan123g  37728  bj-ifan23  37729  bj-ifdfbi  37730  bj-ifdfxor  37732  rp-isfinite6  37744  xpcogend  37773  dfxor4  37789  snhesn  37809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator