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  1824  sbbi  2120  sbnf2  2157  eu1  2275  2eu1  2334  2eu4  2337  2eu6  2339  sbabel  2566  neanior  2652  rexeqbii  2697  r19.26m  2801  reean  2834  2ralor  2837  reu5  2881  reu2  3082  reu3  3084  2reu5lem3  3101  eqss  3323  unss  3481  ralunb  3488  ssin  3523  undi  3548  indifdir  3557  undif3  3562  inab  3569  difab  3570  reuss2  3581  reupick  3585  prss  3912  sstp  3923  tpss  3924  prsspw  3931  prneimg  3938  prnebg  3939  uniin  3995  intun  4042  intpr  4043  disjiun  4162  disjxiun  4169  brin  4219  brdif  4220  ssext  4378  pweqb  4380  opthg2  4397  copsex4g  4405  eqopab2b  4444  pwin  4447  pofun  4479  wetrep  4535  sucelon  4756  elxp3  4887  soinxp  4901  weinxp  4904  relun  4950  inopab  4964  difopab  4965  inxp  4966  opelco2g  4999  cnvco  5015  dmin  5036  intasym  5208  asymref  5209  asymref2  5210  cnvdif  5237  xpnz  5251  xp11  5263  dfco2  5328  relssdmrn  5349  cnvpo  5369  cnvso  5370  xpco  5373  dffun4  5425  funun  5454  fun11  5475  fununi  5476  imadif  5487  fnres  5520  fnopabg  5527  fun  5566  fin  5582  dff1o2  5638  brprcneu  5680  dffv2  5755  fsn  5865  dff1o6  5972  isotr  6015  eqoprab2b  6091  elxp6  6337  difxp  6339  dfoprab3  6362  fsplit  6410  poxp  6417  soxp  6418  brtpos2  6444  porpss  6485  opiota  6494  tfrlem5  6600  tfrlem7  6603  dfer2  6865  eqer  6897  iiner  6935  uniinqs  6943  brecop  6956  eroveu  6958  erovlem  6959  ovec  6973  mapval2  7002  ixpin  7046  boxriin  7063  brsdom  7089  xpcomco  7157  xpassen  7161  sbthlem9  7184  sbthlem10  7185  brsdom2  7190  ssenen  7240  unfi  7333  dffi3  7394  dfsup2  7405  dfsup2OLD  7406  axinf2  7551  zfinf2  7553  oemapso  7594  scottexs  7767  scott0s  7768  kardex  7774  karden  7775  dfac5lem1  7960  dfac5lem3  7962  kmlem15  8000  enfin2i  8157  fin23lem34  8182  brdom7disj  8365  fpwwe2lem12  8472  fpwwe2lem13  8473  axgroth5  8655  grothprim  8665  mulgt0sr  8936  addcnsr  8966  mulcnsr  8967  ltresr  8971  axcnre  8995  1re  9046  ssxr  9101  infmsup  9942  infmrgelb  9944  infmrlb  9945  nnwos  10500  zmin  10526  xrnemnf  10674  xrnepnf  10675  xmullem  10799  xmulcom  10801  xmulneg1  10804  xmulf  10807  xrinfmss2  10845  elfzuzb  11009  fzass4  11046  seqof  11335  hashbclem  11656  hashfacen  11658  rexanre  12105  caubnd  12117  o1lo1  12286  rpnnen2  12780  isprm3  13043  prmreclem2  13240  4sqlem12  13279  isffth2  14068  fucinv  14125  lubid  14394  oduglb  14521  odulub  14523  issubm  14703  isnsg2  14925  oppgid  15107  lsmdisjr  15271  lsmhash  15292  dprd0  15544  dvdsrtr  15712  isirred2  15761  lss1d  15994  lspsolvlem  16169  lbsextlem2  16186  unocv  16862  iunocv  16863  tgval2  16976  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  cnnei  17300  2ndcctbss  17471  txuni2  17550  txbas  17552  ptbasin  17562  txdis1cn  17620  xkococnlem  17644  opnfbas  17827  fgcl  17863  fbasrn  17869  filuni  17870  cfinfil  17878  csdfil  17879  fin1aufil  17917  rnelfmlem  17937  fmfnfmlem3  17941  txflf  17991  xmeterval  18415  reconn  18812  iimulcl  18915  iscau3  19184  minveclem3  19283  pmltpc  19300  ovolfcl  19316  ismbl  19375  dyaddisj  19441  iblre  19638  evlsval  19893  plyun0  20069  logfaclbnd  20959  lgslem3  21035  lgsdir2lem5  21064  nb3grapr2  21416  cusgra3v  21426  4cycl4v4e  21606  4cycl4dv4e  21608  elghom  21904  ajfval  22263  issh  22663  chcon2i  22919  chcon3i  22921  spanuni  22999  5oalem7  23115  3oalem3  23119  pjin2i  23649  pjin3i  23650  cvnbtwn4  23745  mdslj1i  23775  mdslj2i  23776  mdslmd1i  23785  chrelat4i  23829  chirredi  23850  cdj3i  23897  iuninc  23964  suppss2f  24002  fmptdF  24022  mptfnf  24026  disjdsct  24043  tosglb  24145  esumpfinvalf  24419  measiuns  24524  sibfof  24607  ballotlem2  24699  ballotlemodife  24708  derangenlem  24810  pconcon  24871  dftr6  25321  dffr5  25324  dfpo2  25326  fundmpss  25336  elpotr  25351  soseq  25468  wfrlem5  25474  wfrlem11  25480  frrlem5  25499  frrlem5c  25501  nocvxmin  25559  brtxp  25634  brpprod  25639  brsset  25643  idsset  25644  dfon3  25646  ellimits  25664  elfuns  25668  brcart  25685  brapply  25691  brcap  25693  brsuccf  25694  funpartfun  25696  dfrdg4  25703  tfrqfree  25704  altopthc  25720  altopthd  25721  altopelaltxp  25725  outsideoftr  25967  df3nandALT1  26050  imnand2  26053  ismblfin  26146  mbfposadd  26153  trer  26209  gtinf  26212  neibastop1  26278  neifg  26290  inixp  26320  keridl  26532  smprngopr  26552  prtlem10  26604  prter1  26618  mzpclall  26674  mzpincl  26681  mzpindd  26693  2nn0ind  26898  dford4  26990  wopprc  26991  islmodfg  27035  issubmd  27251  gsumcom3  27322  isdomn3  27391  2reu5a  27822  2reu1  27831  2reu4a  27834  f13dfv  27962  frisusgranb  28101  frgra3v  28106  onfrALTlem5  28339  onfrALTlem4  28340  undif3VD  28703  onfrALTlem5VD  28706  onfrALTlem4VD  28707  bnj887  28840  bnj976  28854  bnj1385  28910  bnj153  28957  bnj543  28970  bnj607  28993  bnj882  29003  bnj916  29010  bnj983  29028  sbbiNEW7  29274  sbnf2NEW7  29309  lcvbr3  29506  isopos  29663  llnexatN  30003  snatpsubN  30232  pclclN  30373  pclfinN  30382  lhpocnel2  30501  cdlemk19w  31454  dih1dimatlem  31812
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