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

Theorem anbi12i 680
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 678 . 2  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)
3 anbi12.2 . . 3  |-  ( ch  <->  th )
43anbi2i 677 . 2  |-  ( ( ps  /\  ch )  <->  ( ps  /\  th )
)
52, 4bitri 242 1  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  anbi12ci  681  ordi  836  ordir  837  orddi  841  pm5.17  860  xor  863  3anbi123i  1143  an6  1264  nanbi  1304  cadan  1402  nic-axALT  1449  19.43OLD  1617  sbequ8  1665  nfimdOLD  1830  sbrim  2140  sbbi  2146  sbnf2  2190  eu1  2308  2eu1  2367  2eu4  2370  2eu6  2372  sbabel  2604  neanior  2695  rexeqbii  2742  r19.26m  2847  reean  2880  2ralor  2883  reu5  2927  reu2  3128  reu3  3130  2reu5lem3  3147  eqss  3349  unss  3507  ralunb  3514  ssin  3548  undi  3573  indifdir  3582  undif3  3587  inab  3594  difab  3595  reuss2  3606  reupick  3610  prss  3976  sstp  3987  tpss  3988  prsspw  3995  prneimg  4002  prnebg  4003  uniin  4059  intun  4106  intpr  4107  disjiun  4227  disjxiun  4234  brin  4284  brdif  4285  ssext  4447  pweqb  4449  opthg2  4466  copsex4g  4474  eqopab2b  4513  pwin  4516  pofun  4548  wetrep  4604  sucelon  4826  elxp3  4957  soinxp  4971  weinxp  4974  relun  5020  inopab  5034  difopab  5035  inxp  5036  opelco2g  5069  cnvco  5085  dmin  5106  intasym  5278  asymref  5279  asymref2  5280  cnvdif  5307  xpnz  5321  xp11  5333  dfco2  5398  relssdmrn  5419  cnvpo  5439  cnvso  5440  xpco  5443  dffun4  5495  funun  5524  fun11  5545  fununi  5546  imadif  5557  fnres  5590  fnopabg  5597  fun  5636  fin  5652  dff1o2  5708  brprcneu  5750  dffv2  5825  fsn  5935  dff1o6  6042  isotr  6085  eqoprab2b  6161  elxp6  6407  difxp  6409  dfoprab3  6432  fsplit  6480  poxp  6487  soxp  6488  brtpos2  6514  porpss  6555  opiota  6564  tfrlem5  6670  tfrlem7  6673  dfer2  6935  eqer  6967  iiner  7005  uniinqs  7013  brecop  7026  eroveu  7028  erovlem  7029  ovec  7043  mapval2  7072  ixpin  7116  boxriin  7133  brsdom  7159  xpcomco  7227  xpassen  7231  sbthlem9  7254  sbthlem10  7255  brsdom2  7260  ssenen  7310  unfi  7403  dffi3  7465  dfsup2  7476  dfsup2OLD  7477  axinf2  7624  zfinf2  7626  oemapso  7667  scottexs  7842  scott0s  7843  kardex  7849  karden  7850  dfac5lem1  8035  dfac5lem3  8037  kmlem15  8075  enfin2i  8232  fin23lem34  8257  brdom7disj  8440  fpwwe2lem12  8547  fpwwe2lem13  8548  axgroth5  8730  grothprim  8740  mulgt0sr  9011  addcnsr  9041  mulcnsr  9042  ltresr  9046  axcnre  9070  1re  9121  ssxr  9176  infmsup  10017  infmrgelb  10019  infmrlb  10020  nnwos  10575  zmin  10601  xrnemnf  10749  xrnepnf  10750  xmullem  10874  xmulcom  10876  xmulneg1  10879  xmulf  10882  xrinfmss2  10920  elfzuzb  11084  fzass4  11121  seqof  11411  hashbclem  11732  hashfacen  11734  rexanre  12181  caubnd  12193  o1lo1  12362  rpnnen2  12856  isprm3  13119  prmreclem2  13316  4sqlem12  13355  isffth2  14144  fucinv  14201  lubid  14470  oduglb  14597  odulub  14599  issubm  14779  isnsg2  15001  oppgid  15183  lsmdisjr  15347  lsmhash  15368  dprd0  15620  dvdsrtr  15788  isirred2  15837  lss1d  16070  lspsolvlem  16245  lbsextlem2  16262  unocv  16938  iunocv  16939  tgval2  17052  fctop  17099  cctop  17101  ppttop  17102  epttop  17104  cnnei  17377  2ndcctbss  17549  txuni2  17628  txbas  17630  ptbasin  17640  txdis1cn  17698  xkococnlem  17722  opnfbas  17905  fgcl  17941  fbasrn  17947  filuni  17948  cfinfil  17956  csdfil  17957  fin1aufil  17995  rnelfmlem  18015  fmfnfmlem3  18019  txflf  18069  xmeterval  18493  reconn  18890  iimulcl  18993  iscau3  19262  minveclem3  19361  pmltpc  19378  ovolfcl  19394  ismbl  19453  dyaddisj  19519  iblre  19714  evlsval  19971  plyun0  20147  logfaclbnd  21037  lgslem3  21113  lgsdir2lem5  21142  nb3grapr2  21494  cusgra3v  21504  4cycl4v4e  21684  4cycl4dv4e  21686  elghom  21982  ajfval  22341  issh  22741  chcon2i  22997  chcon3i  22999  spanuni  23077  5oalem7  23193  3oalem3  23197  pjin2i  23727  pjin3i  23728  cvnbtwn4  23823  mdslj1i  23853  mdslj2i  23854  mdslmd1i  23863  chrelat4i  23907  chirredi  23928  cdj3i  23975  iuninc  24042  suppss2f  24080  fmptdF  24100  mptfnf  24104  disjdsct  24121  tosglb  24223  esumpfinvalf  24497  measiuns  24602  sibfof  24685  ballotlem2  24777  ballotlemodife  24786  derangenlem  24888  pconcon  24949  dftr6  25404  dffr5  25407  dfpo2  25409  pocnv  25418  fundmpss  25421  elpotr  25439  soseq  25560  wfrlem5  25573  wfrlem11  25579  frrlem5  25617  frrlem5c  25619  nocvxmin  25677  brtxp  25756  brpprod  25761  brsset  25765  idsset  25766  dfon3  25768  ellimits  25786  dffun10  25790  elfuns  25791  brcart  25808  brimg  25813  brapply  25814  brcap  25816  brsuccf  25817  funpartfun  25819  dfrdg4  25826  tfrqfree  25827  altopthc  25847  altopthd  25848  altopelaltxp  25852  outsideoftr  26094  df3nandALT1  26177  imnand2  26180  ismblfin  26283  mbfposadd  26290  trer  26357  gtinf  26360  neibastop1  26426  neifg  26438  inixp  26468  keridl  26680  smprngopr  26700  prtlem10  26752  prter1  26766  mzpclall  26822  mzpincl  26829  mzpindd  26841  2nn0ind  27046  dford4  27138  wopprc  27139  islmodfg  27182  issubmd  27398  gsumcom3  27469  isdomn3  27538  2reu5a  27969  2reu1  27978  2reu4a  27981  f13dfv  28123  frisusgranb  28485  frgra3v  28490  onfrALTlem5  28726  onfrALTlem4  28727  undif3VD  29092  onfrALTlem5VD  29095  onfrALTlem4VD  29096  bnj887  29232  bnj976  29246  bnj1385  29302  bnj153  29349  bnj543  29362  bnj607  29385  bnj882  29395  bnj916  29402  bnj983  29420  sbbiNEW7  29668  sbnf2NEW7  29706  lcvbr3  29919  isopos  30076  llnexatN  30416  snatpsubN  30645  pclclN  30786  pclfinN  30795  lhpocnel2  30914  cdlemk19w  31867  dih1dimatlem  32225
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 179  df-an 362
  Copyright terms: Public domain W3C validator