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  2097  sbnf2  2134  eu1  2252  2eu1  2311  2eu4  2314  2eu6  2316  sbabel  2542  neanior  2628  rexeqbii  2673  r19.26m  2777  reean  2810  2ralor  2813  reu5  2857  reu2  3058  reu3  3060  2reu5lem3  3077  eqss  3299  unss  3457  ralunb  3464  ssin  3499  undi  3524  indifdir  3533  undif3  3538  inab  3545  difab  3546  reuss2  3557  reupick  3561  prss  3888  sstp  3899  tpss  3900  prsspw  3906  prneimg  3913  prnebg  3914  uniin  3970  intun  4017  intpr  4018  disjiun  4136  disjxiun  4143  brin  4193  brdif  4194  ssext  4352  pweqb  4354  opthg2  4371  copsex4g  4379  eqopab2b  4418  pwin  4421  pofun  4453  wetrep  4509  sucelon  4730  elxp3  4861  soinxp  4875  weinxp  4878  relun  4924  inopab  4938  difopab  4939  inxp  4940  opelco2g  4973  cnvco  4989  dmin  5010  intasym  5182  asymref  5183  asymref2  5184  cnvdif  5211  xpnz  5225  xp11  5237  dfco2  5302  relssdmrn  5323  cnvpo  5343  cnvso  5344  xpco  5347  dffun4  5399  funun  5428  fun11  5449  fununi  5450  imadif  5461  fnres  5494  fnopabg  5501  fun  5540  fin  5556  dff1o2  5612  brprcneu  5654  dffv2  5728  fsn  5838  dff1o6  5945  isotr  5988  eqoprab2b  6064  elxp6  6310  difxp  6312  dfoprab3  6335  fsplit  6383  poxp  6387  soxp  6388  brtpos2  6414  porpss  6455  opiota  6464  tfrlem5  6570  tfrlem7  6573  dfer2  6835  eqer  6867  iiner  6905  uniinqs  6913  brecop  6926  eroveu  6928  erovlem  6929  ovec  6943  mapval2  6972  ixpin  7016  boxriin  7033  brsdom  7059  xpcomco  7127  xpassen  7131  sbthlem9  7154  sbthlem10  7155  brsdom2  7160  ssenen  7210  unfi  7303  dffi3  7364  dfsup2  7375  dfsup2OLD  7376  axinf2  7521  zfinf2  7523  oemapso  7564  scottexs  7737  scott0s  7738  kardex  7744  karden  7745  dfac5lem1  7930  dfac5lem3  7932  kmlem15  7970  enfin2i  8127  fin23lem34  8152  brdom7disj  8335  fpwwe2lem12  8442  fpwwe2lem13  8443  axgroth5  8625  grothprim  8635  mulgt0sr  8906  addcnsr  8936  mulcnsr  8937  ltresr  8941  axcnre  8965  1re  9016  ssxr  9071  infmsup  9911  infmrgelb  9913  infmrlb  9914  nnwos  10469  zmin  10495  xrnemnf  10643  xrnepnf  10644  xmullem  10768  xmulcom  10770  xmulneg1  10773  xmulf  10776  xrinfmss2  10814  elfzuzb  10978  fzass4  11015  seqof  11300  hashbclem  11621  hashfacen  11623  rexanre  12070  caubnd  12082  o1lo1  12251  rpnnen2  12745  isprm3  13008  prmreclem2  13205  4sqlem12  13244  isffth2  14033  fucinv  14090  lubid  14359  oduglb  14486  odulub  14488  issubm  14668  isnsg2  14890  oppgid  15072  lsmdisjr  15236  lsmhash  15257  dprd0  15509  dvdsrtr  15677  isirred2  15726  lss1d  15959  lspsolvlem  16134  lbsextlem2  16151  unocv  16823  iunocv  16824  tgval2  16937  fctop  16984  cctop  16986  ppttop  16987  epttop  16989  cnnei  17261  2ndcctbss  17432  txuni2  17511  txbas  17513  ptbasin  17523  txdis1cn  17581  xkococnlem  17605  opnfbas  17788  fgcl  17824  fbasrn  17830  filuni  17831  cfinfil  17839  csdfil  17840  fin1aufil  17878  rnelfmlem  17898  fmfnfmlem3  17902  txflf  17952  xmeterval  18345  reconn  18723  iimulcl  18826  iscau3  19095  minveclem3  19190  pmltpc  19207  ovolfcl  19223  ismbl  19282  dyaddisj  19348  iblre  19545  evlsval  19800  plyun0  19976  logfaclbnd  20866  lgslem3  20942  lgsdir2lem5  20971  nb3grapr2  21322  cusgra3v  21332  4cycl4v4e  21494  4cycl4dv4e  21496  elghom  21792  ajfval  22151  issh  22551  chcon2i  22807  chcon3i  22809  spanuni  22887  5oalem7  23003  3oalem3  23007  pjin2i  23537  pjin3i  23538  cvnbtwn4  23633  mdslj1i  23663  mdslj2i  23664  mdslmd1i  23673  chrelat4i  23717  chirredi  23738  cdj3i  23785  iuninc  23848  suppss2f  23885  fmptdF  23904  mptfnf  23908  disjdsct  23924  esumpfinvalf  24255  measiuns  24358  ballotlem2  24518  ballotlemodife  24527  derangenlem  24629  pconcon  24690  dftr6  25124  dffr5  25127  dfpo2  25129  fundmpss  25139  elpotr  25154  soseq  25271  wfrlem5  25277  wfrlem11  25283  frrlem5  25302  frrlem5c  25304  nocvxmin  25362  brtxp  25437  brpprod  25442  brsset  25446  idsset  25447  dfon3  25449  ellimits  25467  elfuns  25471  brcart  25488  brapply  25494  brcap  25496  brsuccf  25497  funpartfun  25499  dfrdg4  25506  tfrqfree  25507  altopthc  25523  altopthd  25524  altopelaltxp  25528  outsideoftr  25770  df3nandALT1  25853  imnand2  25856  itg2addnc  25952  trer  26003  gtinf  26006  neibastop1  26072  neifg  26084  inixp  26114  keridl  26326  smprngopr  26346  prtlem10  26398  prter1  26412  mzpclall  26468  mzpincl  26475  mzpindd  26487  2nn0ind  26692  dford4  26784  wopprc  26785  islmodfg  26829  issubmd  27045  gsumcom3  27116  isdomn3  27185  2reu5a  27616  2reu1  27625  2reu4a  27628  frisusgranb  27743  frgra3v  27748  onfrALTlem5  27964  onfrALTlem4  27965  undif3VD  28328  onfrALTlem5VD  28331  onfrALTlem4VD  28332  bnj887  28465  bnj976  28479  bnj1385  28535  bnj153  28582  bnj543  28595  bnj607  28618  bnj882  28628  bnj916  28635  bnj983  28653  sbbiNEW7  28899  sbnf2NEW7  28934  anandii  29083  equvelv  29092  lcvbr3  29189  isopos  29346  llnexatN  29686  snatpsubN  29915  pclclN  30056  pclfinN  30065  lhpocnel2  30184  cdlemk19w  31137  dih1dimatlem  31495
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