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

Theorem anbi12i 678
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 676 . 2  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)
3 anbi12.2 . . 3  |-  ( ch  <->  th )
43anbi2i 675 . 2  |-  ( ( ps  /\  ch )  <->  ( ps  /\  th )
)
52, 4bitri 240 1  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  anbi12ci  679  ordi  834  ordir  835  orddi  839  pm5.17  858  xor  861  3anbi123i  1140  an6  1261  nanbi  1294  cadan  1382  nic-axALT  1429  19.43OLD  1593  nfimd  1761  sbbi  2011  sbnf2  2047  eu1  2164  2eu1  2223  2eu4  2226  2eu6  2228  sbabel  2445  neanior  2531  rexeqbii  2574  r19.26m  2678  reean  2706  2ralor  2709  reu5  2753  reu2  2953  reu3  2955  2reu5lem3  2972  eqss  3194  unss  3349  ralunb  3356  ssin  3391  undi  3416  indifdir  3425  undif3  3429  inab  3436  difab  3437  reuss2  3448  reupick  3452  prss  3769  sstp  3778  tpss  3779  prsspw  3785  uniin  3847  intun  3894  intpr  3895  disjiun  4013  disjxiun  4020  brin  4070  brdif  4071  ssext  4228  pweqb  4230  opthg2  4247  copsex4g  4255  eqopab2b  4294  pwin  4297  pwundifOLD  4301  pofun  4330  wetrep  4386  sucelon  4608  elxp3  4739  soinxp  4754  weinxp  4757  relun  4802  inopab  4816  difopab  4817  inxp  4818  opelco2g  4851  cnvco  4865  dmin  4886  intasym  5058  asymref  5059  asymref2  5060  cnvdif  5087  xpnz  5099  xp11  5111  dfco2  5172  relssdmrn  5193  cnvpo  5213  cnvso  5214  dffun4  5267  funun  5296  fun11  5315  fununi  5316  imadif  5327  fnres  5360  fnopabg  5367  fun  5405  fin  5421  dff1o2  5477  brprcneu  5518  dffv2  5592  fsn  5696  dff1o6  5791  isotr  5833  eqoprab2b  5906  elxp6  6151  difxp  6153  dfoprab3  6176  fsplit  6223  poxp  6227  soxp  6228  brtpos2  6240  porpss  6281  opiota  6290  tfrlem5  6396  tfrlem7  6399  dfer2  6661  eqer  6693  iiner  6731  brecop  6751  eroveu  6753  erovlem  6754  ovec  6768  mapval2  6797  ixpin  6841  boxriin  6858  brsdom  6884  xpcomco  6952  xpassen  6956  sbthlem9  6979  sbthlem10  6980  brsdom2  6985  ssenen  7035  unfi  7124  dffi3  7184  dfsup2  7195  dfsup2OLD  7196  axinf2  7341  zfinf2  7343  oemapso  7384  scottexs  7557  scott0s  7558  kardex  7564  karden  7565  dfac5lem1  7750  dfac5lem3  7752  kmlem15  7790  enfin2i  7947  fin23lem34  7972  brdom7disj  8156  fpwwe2lem12  8263  fpwwe2lem13  8264  axgroth5  8446  grothprim  8456  mulgt0sr  8727  addcnsr  8757  mulcnsr  8758  ltresr  8762  axcnre  8786  1re  8837  ssxr  8892  infmsup  9732  infmrgelb  9734  infmrlb  9735  nnwos  10286  zmin  10312  xrnemnf  10460  xrnepnf  10461  xmullem  10584  xmulcom  10586  xmulneg1  10589  xmulf  10592  xrinfmss2  10629  elfzuzb  10792  fzass4  10829  seqof  11103  hashbclem  11390  hashfacen  11392  rexanre  11830  caubnd  11842  o1lo1  12011  rpnnen2  12504  isprm3  12767  prmreclem2  12964  4sqlem12  13003  isffth2  13790  fucinv  13847  lubid  14116  oduglb  14243  odulub  14245  issubm  14425  isnsg2  14647  oppgid  14829  lsmdisjr  14993  lsmhash  15014  dprd0  15266  dvdsrtr  15434  isirred2  15483  lss1d  15720  lspsolvlem  15895  lbsextlem2  15912  unocv  16580  iunocv  16581  tgval2  16694  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  2ndcctbss  17181  txuni2  17260  txbas  17262  ptbasin  17272  txdis1cn  17329  xkococnlem  17353  opnfbas  17537  fgcl  17573  fbasrn  17579  filuni  17580  cfinfil  17588  csdfil  17589  fin1aufil  17627  rnelfmlem  17647  fmfnfmlem3  17651  txflf  17701  xmeterval  17978  reconn  18333  iimulcl  18435  iscau3  18704  minveclem3  18793  pmltpc  18810  ovolfcl  18826  ismbl  18885  dyaddisj  18951  iblre  19148  evlsval  19403  plyun0  19579  logfaclbnd  20461  lgslem3  20537  lgsdir2lem5  20566  elghom  21030  ajfval  21387  issh  21787  chcon2i  22043  chcon3i  22045  spanuni  22123  5oalem7  22239  3oalem3  22243  pjin2i  22773  pjin3i  22774  cvnbtwn4  22869  mdslj1i  22899  mdslj2i  22900  mdslmd1i  22909  chrelat4i  22953  chirredi  22974  cdj3i  23021  ballotlem2  23047  ballotlemodife  23056  iuninc  23158  suppss2f  23201  fmptdF  23221  mptfnf  23226  disjdsct  23369  esumpfinvalf  23444  measiuns  23544  derangenlem  23702  pconcon  23762  dftr6  24107  dffr5  24110  dfpo2  24112  fundmpss  24122  elpotr  24137  soseq  24254  wfrlem5  24260  wfrlem11  24266  frrlem5  24285  frrlem5c  24287  nocvxmin  24345  brtxp  24420  brpprod  24425  brsset  24429  idsset  24430  dfon3  24432  ellimits  24450  elfuns  24454  brcart  24471  brapply  24477  brcap  24479  brsuccf  24480  funpartfun  24481  funpartfv  24483  dfrdg4  24488  tfrqfree  24489  altopthc  24505  altopthd  24506  altopelaltxp  24510  outsideoftr  24752  df3nandALT1  24835  imnand2  24838  anddi2  24941  albineal  24999  uninqs  25039  elo  25041  isoriso  25212  inposet  25278  definc  25279  dfdir2  25291  vecval1b  25451  vecval3b  25452  dualcat2  25784  issubcata  25846  isntr  25873  trer  26227  gtinf  26234  neibastop1  26308  neifg  26320  inixp  26399  keridl  26657  smprngopr  26677  prtlem10  26733  prter1  26747  mzpclall  26805  mzpincl  26812  mzpindd  26824  2nn0ind  27030  dford4  27122  wopprc  27123  islmodfg  27167  issubmd  27383  gsumcom3  27454  isdomn3  27523  2reu5a  27955  2reu1  27964  2reu4a  27967  prneimg  28073  frgra3v  28180  onfrALTlem5  28307  onfrALTlem4  28308  undif3VD  28658  onfrALTlem5VD  28661  onfrALTlem4VD  28662  bnj887  28795  bnj976  28809  bnj1385  28865  bnj153  28912  bnj543  28925  bnj607  28948  bnj882  28958  bnj916  28965  bnj983  28983  anandii  29107  equvelv  29116  lcvbr3  29213  isopos  29370  llnexatN  29710  snatpsubN  29939  pclclN  30080  pclfinN  30089  lhpocnel2  30208  cdlemk19w  31161  dih1dimatlem  31519
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 177  df-an 360
  Copyright terms: Public domain W3C validator