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

Theorem anbi12i 680
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 678 . 2  |-  ( (
ph  /\  ch )  <->  ( ps  /\  ch )
)
3 anbi12.2 . . 3  |-  ( ch  <->  th )
43anbi2i 677 . 2  |-  ( ( ps  /\  ch )  <->  ( ps  /\  th )
)
52, 4bitri 242 1  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  anbi12ci  681  ordi  836  ordir  837  orddi  841  pm5.17  860  xor  863  3anbi123i  1143  an6  1264  nanbi  1304  cadan  1402  nic-axALT  1449  19.43OLD  1617  nfimdOLD  1829  sbbi  2143  sbnf2  2186  eu1  2304  2eu1  2363  2eu4  2366  2eu6  2368  sbabel  2600  neanior  2691  rexeqbii  2738  r19.26m  2843  reean  2876  2ralor  2879  reu5  2923  reu2  3124  reu3  3126  2reu5lem3  3143  eqss  3365  unss  3523  ralunb  3530  ssin  3565  undi  3590  indifdir  3599  undif3  3604  inab  3611  difab  3612  reuss2  3623  reupick  3627  prss  3954  sstp  3965  tpss  3966  prsspw  3973  prneimg  3980  prnebg  3981  uniin  4037  intun  4084  intpr  4085  disjiun  4204  disjxiun  4211  brin  4261  brdif  4262  ssext  4420  pweqb  4422  opthg2  4439  copsex4g  4447  eqopab2b  4486  pwin  4489  pofun  4521  wetrep  4577  sucelon  4799  elxp3  4930  soinxp  4944  weinxp  4947  relun  4993  inopab  5007  difopab  5008  inxp  5009  opelco2g  5042  cnvco  5058  dmin  5079  intasym  5251  asymref  5252  asymref2  5253  cnvdif  5280  xpnz  5294  xp11  5306  dfco2  5371  relssdmrn  5392  cnvpo  5412  cnvso  5413  xpco  5416  dffun4  5468  funun  5497  fun11  5518  fununi  5519  imadif  5530  fnres  5563  fnopabg  5570  fun  5609  fin  5625  dff1o2  5681  brprcneu  5723  dffv2  5798  fsn  5908  dff1o6  6015  isotr  6058  eqoprab2b  6134  elxp6  6380  difxp  6382  dfoprab3  6405  fsplit  6453  poxp  6460  soxp  6461  brtpos2  6487  porpss  6528  opiota  6537  tfrlem5  6643  tfrlem7  6646  dfer2  6908  eqer  6940  iiner  6978  uniinqs  6986  brecop  6999  eroveu  7001  erovlem  7002  ovec  7016  mapval2  7045  ixpin  7089  boxriin  7106  brsdom  7132  xpcomco  7200  xpassen  7204  sbthlem9  7227  sbthlem10  7228  brsdom2  7233  ssenen  7283  unfi  7376  dffi3  7438  dfsup2  7449  dfsup2OLD  7450  axinf2  7597  zfinf2  7599  oemapso  7640  scottexs  7813  scott0s  7814  kardex  7820  karden  7821  dfac5lem1  8006  dfac5lem3  8008  kmlem15  8046  enfin2i  8203  fin23lem34  8228  brdom7disj  8411  fpwwe2lem12  8518  fpwwe2lem13  8519  axgroth5  8701  grothprim  8711  mulgt0sr  8982  addcnsr  9012  mulcnsr  9013  ltresr  9017  axcnre  9041  1re  9092  ssxr  9147  infmsup  9988  infmrgelb  9990  infmrlb  9991  nnwos  10546  zmin  10572  xrnemnf  10720  xrnepnf  10721  xmullem  10845  xmulcom  10847  xmulneg1  10850  xmulf  10853  xrinfmss2  10891  elfzuzb  11055  fzass4  11092  seqof  11382  hashbclem  11703  hashfacen  11705  rexanre  12152  caubnd  12164  o1lo1  12333  rpnnen2  12827  isprm3  13090  prmreclem2  13287  4sqlem12  13326  isffth2  14115  fucinv  14172  lubid  14441  oduglb  14568  odulub  14570  issubm  14750  isnsg2  14972  oppgid  15154  lsmdisjr  15318  lsmhash  15339  dprd0  15591  dvdsrtr  15759  isirred2  15808  lss1d  16041  lspsolvlem  16216  lbsextlem2  16233  unocv  16909  iunocv  16910  tgval2  17023  fctop  17070  cctop  17072  ppttop  17073  epttop  17075  cnnei  17348  2ndcctbss  17520  txuni2  17599  txbas  17601  ptbasin  17611  txdis1cn  17669  xkococnlem  17693  opnfbas  17876  fgcl  17912  fbasrn  17918  filuni  17919  cfinfil  17927  csdfil  17928  fin1aufil  17966  rnelfmlem  17986  fmfnfmlem3  17990  txflf  18040  xmeterval  18464  reconn  18861  iimulcl  18964  iscau3  19233  minveclem3  19332  pmltpc  19349  ovolfcl  19365  ismbl  19424  dyaddisj  19490  iblre  19687  evlsval  19942  plyun0  20118  logfaclbnd  21008  lgslem3  21084  lgsdir2lem5  21113  nb3grapr2  21465  cusgra3v  21475  4cycl4v4e  21655  4cycl4dv4e  21657  elghom  21953  ajfval  22312  issh  22712  chcon2i  22968  chcon3i  22970  spanuni  23048  5oalem7  23164  3oalem3  23168  pjin2i  23698  pjin3i  23699  cvnbtwn4  23794  mdslj1i  23824  mdslj2i  23825  mdslmd1i  23834  chrelat4i  23878  chirredi  23899  cdj3i  23946  iuninc  24013  suppss2f  24051  fmptdF  24071  mptfnf  24075  disjdsct  24092  tosglb  24194  esumpfinvalf  24468  measiuns  24573  sibfof  24656  ballotlem2  24748  ballotlemodife  24757  derangenlem  24859  pconcon  24920  dftr6  25375  dffr5  25378  dfpo2  25380  pocnv  25389  fundmpss  25392  elpotr  25410  soseq  25531  wfrlem5  25544  wfrlem11  25550  frrlem5  25588  frrlem5c  25590  nocvxmin  25648  brtxp  25727  brpprod  25732  brsset  25736  idsset  25737  dfon3  25739  ellimits  25757  dffun10  25761  elfuns  25762  brcart  25779  brimg  25784  brapply  25785  brcap  25787  brsuccf  25788  funpartfun  25790  dfrdg4  25797  tfrqfree  25798  altopthc  25818  altopthd  25819  altopelaltxp  25823  outsideoftr  26065  df3nandALT1  26148  imnand2  26151  ismblfin  26249  mbfposadd  26256  trer  26321  gtinf  26324  neibastop1  26390  neifg  26402  inixp  26432  keridl  26644  smprngopr  26664  prtlem10  26716  prter1  26730  mzpclall  26786  mzpincl  26793  mzpindd  26805  2nn0ind  27010  dford4  27102  wopprc  27103  islmodfg  27146  issubmd  27362  gsumcom3  27433  isdomn3  27502  2reu5a  27933  2reu1  27942  2reu4a  27945  f13dfv  28087  frisusgranb  28449  frgra3v  28454  onfrALTlem5  28690  onfrALTlem4  28691  undif3VD  29056  onfrALTlem5VD  29059  onfrALTlem4VD  29060  bnj887  29196  bnj976  29210  bnj1385  29266  bnj153  29313  bnj543  29326  bnj607  29349  bnj882  29359  bnj916  29366  bnj983  29384  sbbiNEW7  29632  sbnf2NEW7  29670  lcvbr3  29883  isopos  30040  llnexatN  30380  snatpsubN  30609  pclclN  30750  pclfinN  30759  lhpocnel2  30878  cdlemk19w  31831  dih1dimatlem  32189
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 179  df-an 362
  Copyright terms: Public domain W3C validator