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

Theorem anbi12i 626
Description: Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993.)
Hypotheses
Ref Expression
anbi12.1 (𝜑𝜓)
anbi12.2 (𝜒𝜃)
Assertion
Ref Expression
anbi12i ((𝜑𝜒) ↔ (𝜓𝜃))

Proof of Theorem anbi12i
StepHypRef Expression
1 anbi12.1 . . 3 (𝜑𝜓)
21anbi1i 623 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 anbi12.2 . . 3 (𝜒𝜃)
43anbi2i 622 . 2 ((𝜓𝜒) ↔ (𝜓𝜃))
52, 4bitri 276 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  anbi12ci  627  ordi  1001  ordir  1002  orddi  1005  pm5.17  1007  xor  1010  cases2  1041  3anbi123i  1149  an6  1438  nanbi  1486  cadan  1603  nic-axALT  1668  19.43OLD  1877  sbbi  2311  sbbivOLD  2321  sbnf2  2372  sbbiALT  2609  eubii  2668  cbveuALT  2691  2mo2  2731  2eu4  2740  sbabel  3020  neanior  3114  r19.26m  3178  rexeqbii  3331  reeanlem  3371  2ralor  3375  reu5  3436  reu2  3720  reu3  3722  2reu5a  3739  2reu5lem3  3752  2reu1  3885  eqss  3986  unss  4164  ralunb  4171  ssin  4211  undi  4255  indifdir  4264  undif3  4269  inab  4275  difab  4276  reuss2  4287  reupick  4291  2reu4lem  4468  reuprg  4638  sstp  4766  tpss  4767  prneimg  4784  prnebg  4785  uniin  4857  intun  4906  intpr  4907  disjiun  5050  disjxiun  5060  brin  5115  brdif  5116  ssext  5344  pweqb  5346  opthg2  5368  copsex4g  5382  propeqop  5394  eqopab2bw  5432  eqopab2b  5436  pwin  5451  pofun  5490  wetrep  5547  elxp3  5617  soinxp  5632  weinxp  5635  csbxp  5649  relun  5683  inopab  5700  difopab  5701  inxp  5702  opelco2g  5737  cnvco  5755  dmin  5779  restidsing  5921  intasym  5973  asymref  5974  asymref2  5975  cnvdif  6000  xpnz  6014  difxp  6019  xpdifid  6023  xp11  6030  dfco2  6096  relssdmrn  6119  cnvpo  6136  cnvso  6137  xpco  6138  reu3op  6141  dffun4  6364  funun  6397  fun11  6425  fununi  6426  imadif  6435  fnres  6471  mptfnf  6480  fnopabg  6482  fun  6537  fin  6556  dff1o2  6617  brprcneu  6659  dffv2  6753  fsn  6893  f13dfv  7025  dff1o6  7026  isotr  7081  eqoprab2bw  7216  eqoprab2b  7217  porpss  7443  sucelon  7520  elxp6  7714  dfoprab3  7743  opiota  7748  poxp  7813  soxp  7814  suppvalbr  7825  brtpos2  7889  wfrlem5  7950  wfrfun  7956  tfrlem7  8010  dfer2  8280  eqer  8314  iiner  8359  uniinqs  8367  brecop  8380  eroveu  8382  erovlem  8383  mapval2  8426  ixpin  8476  boxriin  8493  brsdom  8521  xpcomco  8596  xpassen  8600  sbthlem9  8624  sbthlem10  8625  brsdom2  8630  ssenen  8680  unfi  8774  dffi3  8884  dfsup2  8897  infcllem  8940  axinf2  9092  zfinf2  9094  oemapso  9134  scottexs  9305  scott0s  9306  kardex  9312  karden  9313  dfac5lem1  9538  dfac5lem3  9540  kmlem15  9579  enfin2i  9732  fin23lem34  9757  brdom7disj  9942  fpwwe2lem12  10052  fpwwe2lem13  10053  axgroth5  10235  grothprim  10245  addsrpr  10486  mulsrpr  10487  mulgt0sr  10516  addcnsr  10546  mulcnsr  10547  ltresr  10551  axcnre  10575  1re  10630  ssxr  10699  infrenegsup  11613  nnwos  12304  zmin  12333  xrnemnf  12502  xrnepnf  12503  xmullem  12647  xmulcom  12649  xmulneg1  12652  xmulf  12655  xrinfmss2  12694  elfzuzb  12892  fzass4  12935  seqof  13417  hashbclem  13800  hashfacen  13802  xpcogend  14324  trclublem  14345  rexanre  14696  caubnd  14708  o1lo1  14884  rpnnen2lem12  15568  lcmcllem  15930  lcmftp  15970  lcmfunsnlem2  15974  isprm3  16017  prmreclem2  16243  4sqlem12  16282  isffth2  17176  fucinv  17233  lublecllem  17588  oduglb  17739  odulub  17741  issubm  17956  issubmd  17958  isnsg2  18238  cycsubm  18275  oppgid  18414  symgfixf1  18485  pmtrrn2  18508  lsmdisjr  18730  lsmhash  18751  gsumcom3  19018  dprd0  19073  issrg  19177  dvdsrtr  19322  isirred2  19371  lss1d  19655  lspsolvlem  19834  lbsextlem2  19851  evlsval  20217  cnfldfunALT  20474  unocv  20740  iunocv  20741  mpomatmul  20971  cpmidpmat  21397  tgval2  21480  fctop  21528  ppttop  21531  epttop  21533  cnnei  21806  2ndcctbss  21979  txuni2  22089  txbas  22091  ptbasin  22101  txdis1cn  22159  xkococnlem  22183  opnfbas  22366  fgcl  22402  fbasrn  22408  filuni  22409  cfinfil  22417  csdfil  22418  fin1aufil  22456  rnelfmlem  22476  fmfnfmlem3  22480  txflf  22530  xmeterval  22957  reconn  23351  iimulcl  23456  isclmp  23616  iscau3  23796  rrxmvallem  23922  minveclem3  23947  pmltpc  23966  ovolfcl  23982  ismbl  24042  dyaddisj  24112  iblre  24309  plyun0  24702  logfaclbnd  25712  lgslem3  25789  lgsdir2lem5  25819  tgjustf  26173  ishpg  26459  usgrexmpllem  26956  nb3grpr2  27079  vtxd0nedgb  27184  wlk1walk  27334  clwlkcompbp  27477  wwlknllvtx  27538  wwlksonvtx  27547  wspthnonp  27551  wwlksn0s  27553  wwlksnndef  27597  wwlksnfiOLD  27599  2wlkdlem8  27626  elwwlks2s3  27644  clwwlkf1  27742  clwwlknonccat  27789  clwwlknon2x  27796  3pthdlem1  27857  upgr4cycl4dv4e  27878  frgr2wwlk1  28022  frgrreg  28087  ajfval  28500  issh  28899  chcon2i  29155  chcon3i  29157  spanuni  29235  5oalem7  29351  3oalem3  29355  pjin2i  29884  pjin3i  29885  cvnbtwn4  29980  mdslj1i  30010  mdslj2i  30011  mdslmd1i  30020  chrelat4i  30064  chirredi  30085  cdj3i  30132  rmoun  30172  difrab2  30175  eqdif  30195  inpr0  30206  iuninc  30227  fcoinvbr  30273  suppss2f  30299  fmptdF  30316  disjdsct  30351  cnvoprabOLD  30369  f1od2  30370  hashxpe  30442  tosglblem  30570  pmtrprfv2  30646  ccfldextdgrr  30943  ordtconnlem1  31053  esumpfinvalf  31221  esum2dlem  31237  measiuns  31362  eulerpartlemt0  31513  eulerpartlemr  31518  eulerpartlemn  31525  ballotlem2  31632  ballotlemodife  31641  bnj887  31922  bnj976  31935  bnj1385  31990  bnj153  32038  bnj543  32051  bnj607  32074  bnj882  32084  bnj916  32091  bnj983  32109  derangenlem  32302  pconnconn  32362  fmlaomn0  32521  fmla0disjsuc  32529  fmlasucdisj  32530  elmpst  32667  dftr6  32870  dffr5  32873  dfpo2  32875  fundmpss  32893  elpotr  32910  soseq  32980  frrlem9  33015  fprlem1  33021  frrlem15  33026  nocvxmin  33132  sltrec  33162  brtxp  33225  brpprod  33230  brsset  33234  idsset  33235  dfon3  33237  ellimits  33255  dffun10  33259  elfuns  33260  brcart  33277  brimg  33282  brapply  33283  brcap  33285  brsuccf  33286  funpartfun  33288  dfrecs2  33295  dfrdg4  33296  altopthc  33316  altopthd  33317  altopelaltxp  33321  outsideoftr  33474  trer  33548  neibastop1  33591  neifg  33603  df3nandALT1  33631  imnand2  33634  bj-eldiag2  34348  bj-imdirid  34354  topdifinfeq  34500  relowlssretop  34513  relowlpssretop  34514  wl-cases2-dnf  34621  wl-dfreusb  34724  wl-dfreuv  34725  wl-dfrabv  34729  poimirlem30  34789  poimirlem32  34791  ismblfin  34800  mbfposadd  34806  inixp  34871  elghomOLD  35033  keridl  35178  smprngopr  35198  sbcani  35254  an2anr  35366  inxpxrn  35510  dfcoss2  35528  1cossres  35541  dfcoels  35542  br1cossinres  35554  br1cossinidres  35556  br1cossincnvepres  35557  br1cossxrnidres  35558  br1cossxrncnvepres  35559  cosscnvssid3  35583  coss0  35586  cossid  35587  trcoss  35589  eleccossin  35590  dfssr2  35606  br1cossxrncnvssrres  35615  refsymrels3  35669  refsymrel2  35670  refsymrel3  35671  elrefsymrels3  35673  dfeqvrel2  35692  dfeqvrel3  35693  redundeq1  35731  redundpbi1  35733  dfmember3  35775  eqvreldmqs  35776  dfeldisj3  35819  prtlem10  35868  prter1  35882  lcvbr3  36026  isopos  36183  llnexatN  36524  snatpsubN  36753  pclclN  36894  pclfinN  36903  lhpocnel2  37022  cdlemk19w  37975  dih1dimatlem  38332  psspwb  38979  mzpclall  39189  mzpincl  39196  mzpindd  39208  2nn0ind  39407  dford4  39491  wopprc  39492  islmodfg  39534  isdomn3  39669  ifpan123g  39689  ifpan23  39690  ifpdfbi  39704  ifpnot23  39709  ifpdfxor  39718  ifpidg  39722  ifpid1g  39725  ifpim23g  39726  ifpim123g  39731  ifpim1g  39732  ifp1bi  39733  ifpimimb  39735  ifpororb  39736  ifpor123g  39739  ifpbibib  39741  rp-isfinite6  39749  alephiso2  39782  undmrnresiss  39829  cotrintab  39839  brtrclfv2  39937  dfxor4  39976  snhesn  39997  dffrege76  40150  uneqsn  40238  expandan  40489  ismnuprim  40495  nzin  40515  onfrALTlem5  40741  onfrALTlem4  40742  undif3VD  41081  onfrALTlem5VD  41084  onfrALTlem4VD  41085  ndisj2  41178  rexabsle  41558  ellimcabssub0  41763  limsupre2mpt  41876  limsupre3  41879  limsupre3mpt  41880  limsupre3uz  41882  limsupreuz  41883  liminfreuz  41949  fourierdlem103  42360  fourierdlem104  42361  fourierdlem112  42369  smflim  42919  smflim2  42946  smflimsuplem1  42960  smflimsup  42968  2reu8i  43178  ichan  43462  issubmgm  43888  rabsubmgmd  43890  2zlidl  44037  mndpsuppss  44251  islininds2  44371  zlmodzxzldeplem3  44389  2itscp  44600  alsi-no-surprise  44729
  Copyright terms: Public domain W3C validator