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  1596  nfimd  1773  sbbi  2024  sbnf2  2060  eu1  2177  2eu1  2236  2eu4  2239  2eu6  2241  sbabel  2458  neanior  2544  rexeqbii  2587  r19.26m  2691  reean  2719  2ralor  2722  reu5  2766  reu2  2966  reu3  2968  2reu5lem3  2985  eqss  3207  unss  3362  ralunb  3369  ssin  3404  undi  3429  indifdir  3438  undif3  3442  inab  3449  difab  3450  reuss2  3461  reupick  3465  prss  3785  sstp  3794  tpss  3795  prsspw  3801  uniin  3863  intun  3910  intpr  3911  disjiun  4029  disjxiun  4036  brin  4086  brdif  4087  ssext  4244  pweqb  4246  opthg2  4263  copsex4g  4271  eqopab2b  4310  pwin  4313  pwundifOLD  4317  pofun  4346  wetrep  4402  sucelon  4624  elxp3  4755  soinxp  4770  weinxp  4773  relun  4818  inopab  4832  difopab  4833  inxp  4834  opelco2g  4867  cnvco  4881  dmin  4902  intasym  5074  asymref  5075  asymref2  5076  cnvdif  5103  xpnz  5115  xp11  5127  dfco2  5188  relssdmrn  5209  cnvpo  5229  cnvso  5230  dffun4  5283  funun  5312  fun11  5331  fununi  5332  imadif  5343  fnres  5376  fnopabg  5383  fun  5421  fin  5437  dff1o2  5493  brprcneu  5534  dffv2  5608  fsn  5712  dff1o6  5807  isotr  5849  eqoprab2b  5922  elxp6  6167  difxp  6169  dfoprab3  6192  fsplit  6239  poxp  6243  soxp  6244  brtpos2  6256  porpss  6297  opiota  6306  tfrlem5  6412  tfrlem7  6415  dfer2  6677  eqer  6709  iiner  6747  brecop  6767  eroveu  6769  erovlem  6770  ovec  6784  mapval2  6813  ixpin  6857  boxriin  6874  brsdom  6900  xpcomco  6968  xpassen  6972  sbthlem9  6995  sbthlem10  6996  brsdom2  7001  ssenen  7051  unfi  7140  dffi3  7200  dfsup2  7211  dfsup2OLD  7212  axinf2  7357  zfinf2  7359  oemapso  7400  scottexs  7573  scott0s  7574  kardex  7580  karden  7581  dfac5lem1  7766  dfac5lem3  7768  kmlem15  7806  enfin2i  7963  fin23lem34  7988  brdom7disj  8172  fpwwe2lem12  8279  fpwwe2lem13  8280  axgroth5  8462  grothprim  8472  mulgt0sr  8743  addcnsr  8773  mulcnsr  8774  ltresr  8778  axcnre  8802  1re  8853  ssxr  8908  infmsup  9748  infmrgelb  9750  infmrlb  9751  nnwos  10302  zmin  10328  xrnemnf  10476  xrnepnf  10477  xmullem  10600  xmulcom  10602  xmulneg1  10605  xmulf  10608  xrinfmss2  10645  elfzuzb  10808  fzass4  10845  seqof  11119  hashbclem  11406  hashfacen  11408  rexanre  11846  caubnd  11858  o1lo1  12027  rpnnen2  12520  isprm3  12783  prmreclem2  12980  4sqlem12  13019  isffth2  13806  fucinv  13863  lubid  14132  oduglb  14259  odulub  14261  issubm  14441  isnsg2  14663  oppgid  14845  lsmdisjr  15009  lsmhash  15030  dprd0  15282  dvdsrtr  15450  isirred2  15499  lss1d  15736  lspsolvlem  15911  lbsextlem2  15928  unocv  16596  iunocv  16597  tgval2  16710  fctop  16757  cctop  16759  ppttop  16760  epttop  16762  2ndcctbss  17197  txuni2  17276  txbas  17278  ptbasin  17288  txdis1cn  17345  xkococnlem  17369  opnfbas  17553  fgcl  17589  fbasrn  17595  filuni  17596  cfinfil  17604  csdfil  17605  fin1aufil  17643  rnelfmlem  17663  fmfnfmlem3  17667  txflf  17717  xmeterval  17994  reconn  18349  iimulcl  18451  iscau3  18720  minveclem3  18809  pmltpc  18826  ovolfcl  18842  ismbl  18901  dyaddisj  18967  iblre  19164  evlsval  19419  plyun0  19595  logfaclbnd  20477  lgslem3  20553  lgsdir2lem5  20582  elghom  21046  ajfval  21403  issh  21803  chcon2i  22059  chcon3i  22061  spanuni  22139  5oalem7  22255  3oalem3  22259  pjin2i  22789  pjin3i  22790  cvnbtwn4  22885  mdslj1i  22915  mdslj2i  22916  mdslmd1i  22925  chrelat4i  22969  chirredi  22990  cdj3i  23037  ballotlem2  23063  ballotlemodife  23072  iuninc  23174  suppss2f  23216  fmptdF  23236  mptfnf  23241  disjdsct  23384  esumpfinvalf  23459  measiuns  23559  derangenlem  23717  pconcon  23777  dftr6  24177  dffr5  24180  dfpo2  24182  fundmpss  24192  elpotr  24207  soseq  24324  wfrlem5  24330  wfrlem11  24336  frrlem5  24355  frrlem5c  24357  nocvxmin  24415  brtxp  24490  brpprod  24495  brsset  24499  idsset  24500  dfon3  24502  ellimits  24520  elfuns  24524  brcart  24541  brapply  24547  brcap  24549  brsuccf  24550  funpartfun  24552  dfrdg4  24559  tfrqfree  24560  altopthc  24576  altopthd  24577  altopelaltxp  24581  outsideoftr  24823  df3nandALT1  24906  imnand2  24909  itg2addnc  25004  anddi2  25043  albineal  25101  uninqs  25141  elo  25143  isoriso  25314  inposet  25380  definc  25381  dfdir2  25393  vecval1b  25553  vecval3b  25554  dualcat2  25886  issubcata  25948  isntr  25975  trer  26329  gtinf  26336  neibastop1  26410  neifg  26422  inixp  26501  keridl  26759  smprngopr  26779  prtlem10  26835  prter1  26849  mzpclall  26907  mzpincl  26914  mzpindd  26926  2nn0ind  27132  dford4  27224  wopprc  27225  islmodfg  27269  issubmd  27485  gsumcom3  27556  isdomn3  27625  2reu5a  28057  2reu1  28066  2reu4a  28069  prneimg  28182  nb3grapr2  28289  cusgra3v  28298  4cycl4v4e  28411  4cycl4dv4e  28413  frgra3v  28425  onfrALTlem5  28605  onfrALTlem4  28606  undif3VD  28973  onfrALTlem5VD  28976  onfrALTlem4VD  28977  bnj887  29110  bnj976  29124  bnj1385  29180  bnj153  29227  bnj543  29240  bnj607  29263  bnj882  29273  bnj916  29280  bnj983  29298  sbbiNEW7  29544  sbnf2NEW7  29579  anandii  29729  equvelv  29738  lcvbr3  29835  isopos  29992  llnexatN  30332  snatpsubN  30561  pclclN  30702  pclfinN  30711  lhpocnel2  30830  cdlemk19w  31783  dih1dimatlem  32141
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