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  24178  dffr5  24181  dfpo2  24183  fundmpss  24193  elpotr  24208  soseq  24325  wfrlem5  24331  wfrlem11  24337  frrlem5  24356  frrlem5c  24358  nocvxmin  24416  brtxp  24491  brpprod  24496  brsset  24500  idsset  24501  dfon3  24503  ellimits  24521  elfuns  24525  brcart  24542  brapply  24548  brcap  24550  brsuccf  24551  funpartfun  24553  dfrdg4  24560  tfrqfree  24561  altopthc  24577  altopthd  24578  altopelaltxp  24582  outsideoftr  24824  df3nandALT1  24907  imnand2  24910  itg2addnc  25005  anddi2  25044  albineal  25102  uninqs  25142  elo  25144  isoriso  25315  inposet  25381  definc  25382  dfdir2  25394  vecval1b  25554  vecval3b  25555  dualcat2  25887  issubcata  25949  isntr  25976  trer  26330  gtinf  26337  neibastop1  26411  neifg  26423  inixp  26502  keridl  26760  smprngopr  26780  prtlem10  26836  prter1  26850  mzpclall  26908  mzpincl  26915  mzpindd  26927  2nn0ind  27133  dford4  27225  wopprc  27226  islmodfg  27270  issubmd  27486  gsumcom3  27557  isdomn3  27626  2reu5a  28058  2reu1  28067  2reu4a  28070  prneimg  28183  nb3grapr2  28290  cusgra3v  28299  4cycl4v4e  28412  4cycl4dv4e  28414  frgra3v  28426  onfrALTlem5  28606  onfrALTlem4  28607  undif3VD  28974  onfrALTlem5VD  28977  onfrALTlem4VD  28978  bnj887  29111  bnj976  29125  bnj1385  29181  bnj153  29228  bnj543  29241  bnj607  29264  bnj882  29274  bnj916  29281  bnj983  29299  sbbiNEW7  29545  sbnf2NEW7  29580  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