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

Theorem anbi12i 679
Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
anbi12.1  |-  ( ph  <->  ps )
anbi12.2  |-  ( ch  <->  th )
Assertion
Ref Expression
anbi12i  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)

Proof of Theorem anbi12i
StepHypRef Expression
1 anbi12.1 . . 3  |-  ( ph  <->  ps )
21anbi1i 677 . 2  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)
3 anbi12.2 . . 3  |-  ( ch  <->  th )
43anbi2i 676 . 2  |-  ( ( ps  /\  ch )  <->  ( ps  /\  th )
)
52, 4bitri 241 1  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  anbi12ci  680  ordi  835  ordir  836  orddi  840  pm5.17  859  xor  862  3anbi123i  1142  an6  1263  nanbi  1300  cadan  1398  nic-axALT  1445  19.43OLD  1613  nfimdOLD  1818  sbbi  2104  sbnf2  2141  eu1  2259  2eu1  2318  2eu4  2321  2eu6  2323  sbabel  2549  neanior  2635  rexeqbii  2680  r19.26m  2784  reean  2817  2ralor  2820  reu5  2864  reu2  3065  reu3  3067  2reu5lem3  3084  eqss  3306  unss  3464  ralunb  3471  ssin  3506  undi  3531  indifdir  3540  undif3  3545  inab  3552  difab  3553  reuss2  3564  reupick  3568  prss  3895  sstp  3906  tpss  3907  prsspw  3913  prneimg  3920  prnebg  3921  uniin  3977  intun  4024  intpr  4025  disjiun  4143  disjxiun  4150  brin  4200  brdif  4201  ssext  4359  pweqb  4361  opthg2  4378  copsex4g  4386  eqopab2b  4425  pwin  4428  pofun  4460  wetrep  4516  sucelon  4737  elxp3  4868  soinxp  4882  weinxp  4885  relun  4931  inopab  4945  difopab  4946  inxp  4947  opelco2g  4980  cnvco  4996  dmin  5017  intasym  5189  asymref  5190  asymref2  5191  cnvdif  5218  xpnz  5232  xp11  5244  dfco2  5309  relssdmrn  5330  cnvpo  5350  cnvso  5351  xpco  5354  dffun4  5406  funun  5435  fun11  5456  fununi  5457  imadif  5468  fnres  5501  fnopabg  5508  fun  5547  fin  5563  dff1o2  5619  brprcneu  5661  dffv2  5735  fsn  5845  dff1o6  5952  isotr  5995  eqoprab2b  6071  elxp6  6317  difxp  6319  dfoprab3  6342  fsplit  6390  poxp  6394  soxp  6395  brtpos2  6421  porpss  6462  opiota  6471  tfrlem5  6577  tfrlem7  6580  dfer2  6842  eqer  6874  iiner  6912  uniinqs  6920  brecop  6933  eroveu  6935  erovlem  6936  ovec  6950  mapval2  6979  ixpin  7023  boxriin  7040  brsdom  7066  xpcomco  7134  xpassen  7138  sbthlem9  7161  sbthlem10  7162  brsdom2  7167  ssenen  7217  unfi  7310  dffi3  7371  dfsup2  7382  dfsup2OLD  7383  axinf2  7528  zfinf2  7530  oemapso  7571  scottexs  7744  scott0s  7745  kardex  7751  karden  7752  dfac5lem1  7937  dfac5lem3  7939  kmlem15  7977  enfin2i  8134  fin23lem34  8159  brdom7disj  8342  fpwwe2lem12  8449  fpwwe2lem13  8450  axgroth5  8632  grothprim  8642  mulgt0sr  8913  addcnsr  8943  mulcnsr  8944  ltresr  8948  axcnre  8972  1re  9023  ssxr  9078  infmsup  9918  infmrgelb  9920  infmrlb  9921  nnwos  10476  zmin  10502  xrnemnf  10650  xrnepnf  10651  xmullem  10775  xmulcom  10777  xmulneg1  10780  xmulf  10783  xrinfmss2  10821  elfzuzb  10985  fzass4  11022  seqof  11307  hashbclem  11628  hashfacen  11630  rexanre  12077  caubnd  12089  o1lo1  12258  rpnnen2  12752  isprm3  13015  prmreclem2  13212  4sqlem12  13251  isffth2  14040  fucinv  14097  lubid  14366  oduglb  14493  odulub  14495  issubm  14675  isnsg2  14897  oppgid  15079  lsmdisjr  15243  lsmhash  15264  dprd0  15516  dvdsrtr  15684  isirred2  15733  lss1d  15966  lspsolvlem  16141  lbsextlem2  16158  unocv  16830  iunocv  16831  tgval2  16944  fctop  16991  cctop  16993  ppttop  16994  epttop  16996  cnnei  17268  2ndcctbss  17439  txuni2  17518  txbas  17520  ptbasin  17530  txdis1cn  17588  xkococnlem  17612  opnfbas  17795  fgcl  17831  fbasrn  17837  filuni  17838  cfinfil  17846  csdfil  17847  fin1aufil  17885  rnelfmlem  17905  fmfnfmlem3  17909  txflf  17959  xmeterval  18352  reconn  18730  iimulcl  18833  iscau3  19102  minveclem3  19197  pmltpc  19214  ovolfcl  19230  ismbl  19289  dyaddisj  19355  iblre  19552  evlsval  19807  plyun0  19983  logfaclbnd  20873  lgslem3  20949  lgsdir2lem5  20978  nb3grapr2  21329  cusgra3v  21339  4cycl4v4e  21501  4cycl4dv4e  21503  elghom  21799  ajfval  22158  issh  22558  chcon2i  22814  chcon3i  22816  spanuni  22894  5oalem7  23010  3oalem3  23014  pjin2i  23544  pjin3i  23545  cvnbtwn4  23640  mdslj1i  23670  mdslj2i  23671  mdslmd1i  23680  chrelat4i  23724  chirredi  23745  cdj3i  23792  iuninc  23855  suppss2f  23892  fmptdF  23911  mptfnf  23915  disjdsct  23931  esumpfinvalf  24262  measiuns  24365  ballotlem2  24525  ballotlemodife  24534  derangenlem  24636  pconcon  24697  dftr6  25131  dffr5  25134  dfpo2  25136  fundmpss  25146  elpotr  25161  soseq  25278  wfrlem5  25284  wfrlem11  25290  frrlem5  25309  frrlem5c  25311  nocvxmin  25369  brtxp  25444  brpprod  25449  brsset  25453  idsset  25454  dfon3  25456  ellimits  25474  elfuns  25478  brcart  25495  brapply  25501  brcap  25503  brsuccf  25504  funpartfun  25506  dfrdg4  25513  tfrqfree  25514  altopthc  25530  altopthd  25531  altopelaltxp  25535  outsideoftr  25777  df3nandALT1  25860  imnand2  25863  itg2addnc  25959  trer  26010  gtinf  26013  neibastop1  26079  neifg  26091  inixp  26121  keridl  26333  smprngopr  26353  prtlem10  26405  prter1  26419  mzpclall  26475  mzpincl  26482  mzpindd  26494  2nn0ind  26699  dford4  26791  wopprc  26792  islmodfg  26836  issubmd  27052  gsumcom3  27123  isdomn3  27192  2reu5a  27623  2reu1  27632  2reu4a  27635  frisusgranb  27750  frgra3v  27755  onfrALTlem5  27971  onfrALTlem4  27972  undif3VD  28335  onfrALTlem5VD  28338  onfrALTlem4VD  28339  bnj887  28472  bnj976  28486  bnj1385  28542  bnj153  28589  bnj543  28602  bnj607  28625  bnj882  28635  bnj916  28642  bnj983  28660  sbbiNEW7  28906  sbnf2NEW7  28941  lcvbr3  29138  isopos  29295  llnexatN  29635  snatpsubN  29864  pclclN  30005  pclfinN  30014  lhpocnel2  30133  cdlemk19w  31086  dih1dimatlem  31444
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