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

Theorem anbi12i 627
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 624 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 anbi12.2 . . 3 (𝜒𝜃)
43anbi2i 623 . 2 ((𝜓𝜒) ↔ (𝜓𝜃))
52, 4bitri 274 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 205  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 206  df-an 397
This theorem is referenced by:  anbi12ci  628  an2anr  635  ordi  1004  ordir  1005  orddi  1008  pm5.17  1010  xor  1013  cases2  1046  3anbi123i  1155  an6  1445  nanbi  1498  cadan  1610  nic-axALT  1676  19.43OLD  1886  sbbi  2304  aaan  2327  sbnf2  2354  eubii  2583  cbveuvw  2604  cbveuw  2605  cbveuALT  2608  2mo2  2647  2eu4  2654  sbabel  2941  sbabelOLD  2942  neanior  3037  r19.26m  3113  reeanlem  3216  2ralorOLD  3220  rexeqbii  3316  reu5  3355  cbvreuw  3383  reu2  3683  reu3  3685  2reu5a  3702  2reu5lem3  3715  2reu1  3853  eqss  3959  ss2abdv  4020  unss  4144  ralunb  4151  ssin  4190  undi  4234  indifdi  4243  indifdirOLD  4245  undif3  4250  inab  4259  difab  4260  reuss2  4275  reupick  4278  2reu4lem  4483  reuprg  4664  sstp  4794  tpss  4795  prneimg  4812  prnebg  4813  uniin  4892  intun  4941  intprOLD  4944  disjiun  5092  disjxiun  5102  brin  5157  brdif  5158  ssext  5411  pweqb  5413  opthg2  5436  copsex4g  5452  propeqop  5464  eqopab2bw  5505  eqopab2b  5509  pwin  5527  pofun  5563  dffr6  5591  wetrep  5626  elxp3  5698  soinxp  5713  weinxp  5716  csbxp  5731  relun  5767  inopab  5785  difopab  5786  difopabOLD  5787  inxp  5788  opelco2g  5823  cnvco  5841  dmin  5867  restidsing  6006  intasym  6069  asymref  6070  asymref2  6071  cnvdif  6096  xpnz  6111  difxp  6116  xpdifid  6120  xp11  6127  dfco2  6197  relssdmrnOLD  6221  cnvpo  6239  cnvso  6240  xpco  6241  reu3op  6244  dfpo2  6248  dffun4  6512  funun  6547  fun11  6575  fununi  6576  imadif  6585  fnres  6628  mptfnf  6636  fnopabg  6638  fun  6704  fin  6722  dff1o2  6789  brprcneu  6832  brprcneuALT  6833  dffv2  6936  fsn  7081  f13dfv  7220  dff1o6  7221  isotr  7281  eqoprab2bw  7427  eqoprab2b  7428  fvmpopr2d  7516  porpss  7664  epweon  7709  onsucb  7752  elxp6  7955  dfoprab3  7986  opiota  7991  poxp  8060  soxp  8061  poxp2  8075  xpord2pred  8077  xpord2indlem  8079  xpord3pred  8084  xpord3inddlem  8086  soseq  8091  suppvalbr  8096  brtpos2  8163  frrlem9  8225  fprlem1  8231  wfrlem5OLD  8259  wfrfunOLD  8265  tfrlem7  8329  dfer2  8649  eqer  8683  iiner  8728  uniinqs  8736  brecop  8749  eroveu  8751  erovlem  8752  fsetexb  8802  mapval2  8810  ixpin  8861  boxriin  8878  brsdom  8915  xpcomco  9006  xpassen  9010  sbthlem9  9035  sbthlem10  9036  brsdom2  9041  ssenen  9095  sbthfilem  9145  unfiOLD  9257  dffi3  9367  dfsup2  9380  infcllem  9423  axinf2  9576  zfinf2  9578  oemapso  9618  ttrcltr  9652  frrlem15  9693  scottexs  9823  scott0s  9824  kardex  9830  karden  9831  dfac5lem1  10059  dfac5lem3  10061  kmlem15  10100  enfin2i  10257  fin23lem34  10282  brdom7disj  10467  fpwwe2lem11  10577  fpwwe2lem12  10578  axgroth5  10760  grothprim  10770  addsrpr  11011  mulsrpr  11012  mulgt0sr  11041  addcnsr  11071  mulcnsr  11072  ltresr  11076  axcnre  11100  1re  11155  ssxr  11224  infrenegsup  12138  nnwos  12840  zmin  12869  xrnemnf  13038  xrnepnf  13039  xmullem  13183  xmulcom  13185  xmulneg1  13188  xmulf  13191  xrinfmss2  13230  elfzuzb  13435  fzass4  13479  seqof  13965  hashbclem  14349  hashfacen  14351  hashfacenOLD  14352  xpcogend  14859  trclublem  14880  rexanre  15231  caubnd  15243  o1lo1  15419  rpnnen2lem12  16107  lcmcllem  16472  lcmftp  16512  lcmfunsnlem2  16516  isprm3  16559  prmreclem2  16789  4sqlem12  16828  catcone0  17567  isffth2  17803  fucinv  17862  lublecllem  18249  odulub  18296  oduglb  18298  issubm  18614  issubmd  18617  0subm  18628  insubm  18629  sursubmefmnd  18706  injsubmefmnd  18707  smndex1mgm  18717  isnsg2  18958  cycsubm  18995  oppgid  19137  symgfixf1  19219  pmtrrn2  19242  lsmdisjr  19466  lsmhash  19487  gsumcom3  19755  dprd0  19810  issrg  19919  dvdsrtr  20081  isirred2  20130  lss1d  20424  lspsolvlem  20603  lbsextlem2  20620  cnfldfun  20808  unocv  21084  iunocv  21085  evlsval  21496  mpomatmul  21795  cpmidpmat  22222  tgval2  22306  fctop  22354  ppttop  22357  epttop  22359  cnnei  22633  2ndcctbss  22806  txuni2  22916  txbas  22918  ptbasin  22928  txdis1cn  22986  xkococnlem  23010  opnfbas  23193  fgcl  23229  fbasrn  23235  filuni  23236  cfinfil  23244  csdfil  23245  fin1aufil  23283  rnelfmlem  23303  fmfnfmlem3  23307  txflf  23357  xmeterval  23785  reconn  24191  iimulcl  24300  isclmp  24460  iscau3  24642  rrxmvallem  24768  minveclem3  24793  pmltpc  24814  ovolfcl  24830  ismbl  24890  dyaddisj  24960  iblre  25158  plyun0  25558  logfaclbnd  26570  lgslem3  26647  lgsdir2lem5  26677  nosupinfsep  27080  nocvxmin  27118  sltrec  27159  madebdaylemlrcut  27228  addsproplem2  27282  addsunif  27310  negsproplem2  27327  negsid  27339  tgjustf  27415  ishpg  27701  usgrexmpllem  28208  nb3grpr2  28331  vtxd0nedgb  28436  wlk1walk  28587  clwlkcompbp  28730  wwlknllvtx  28791  wwlksonvtx  28800  wspthnonp  28804  wwlksn0s  28806  wwlksnndef  28850  2wlkdlem8  28878  elwwlks2s3  28896  clwwlkf1  28993  clwwlknonccat  29040  clwwlknon2x  29047  3pthdlem1  29108  upgr4cycl4dv4e  29129  frgr2wwlk1  29273  frgrreg  29338  ajfval  29751  issh  30150  chcon2i  30406  chcon3i  30408  spanuni  30486  5oalem7  30602  3oalem3  30606  pjin2i  31135  pjin3i  31136  cvnbtwn4  31231  mdslj1i  31261  mdslj2i  31262  mdslmd1i  31271  chrelat4i  31315  chirredi  31336  cdj3i  31383  rmoun  31422  difrab2  31426  eqdif  31446  inpr0  31459  iuninc  31479  fcoinvbr  31526  suppss2f  31553  fmptdF  31572  disjdsct  31616  cnvoprabOLD  31637  f1od2  31638  hashxpe  31709  tosglblem  31834  mgcval  31847  pmtrprfv2  31939  ssmxidllem  32238  ccfldextdgrr  32356  ordtconnlem1  32505  esumpfinvalf  32675  esum2dlem  32691  measiuns  32816  eulerpartlemt0  32969  eulerpartlemr  32974  eulerpartlemn  32981  ballotlem2  33088  ballotlemodife  33097  bnj887  33377  bnj976  33389  bnj1385  33444  bnj153  33492  bnj543  33505  bnj607  33528  bnj882  33538  bnj916  33545  bnj983  33563  derangenlem  33765  pconnconn  33825  fmlaomn0  33984  fmla0disjsuc  33992  fmlasucdisj  33993  elmpst  34130  xpab  34297  dftr6  34324  dffr5  34327  fundmpss  34341  elpotr  34356  brtxp  34465  brpprod  34470  brsset  34474  idsset  34475  dfon3  34477  ellimits  34495  dffun10  34499  elfuns  34500  brcart  34517  brimg  34522  brapply  34523  brcap  34525  brsuccf  34526  funpartfun  34528  dfrecs2  34535  dfrdg4  34536  altopthc  34556  altopthd  34557  altopelaltxp  34561  outsideoftr  34714  trer  34788  neibastop1  34831  neifg  34843  df3nandALT1  34871  imnand2  34874  eliminable-abelab  35336  bj-eldiag2  35648  bj-imdiridlem  35656  bj-opabco  35659  bj-xpcossxp  35660  topdifinfeq  35821  relowlssretop  35834  relowlpssretop  35835  wl-cases2-dnf  35971  poimirlem30  36108  poimirlem32  36110  ismblfin  36119  mbfposadd  36125  inixp  36187  elghomOLD  36346  keridl  36491  smprngopr  36511  sbcani  36567  inxpxrn  36857  dfcoss2  36875  cosscnv  36878  coss1cnvres  36879  coss2cnvepres  36880  1cossres  36891  dfcoels  36892  trressn  36907  br1cossinres  36909  br1cossinidres  36911  br1cossincnvepres  36912  br1cossxrnidres  36913  br1cossxrncnvepres  36914  cosscnvssid3  36938  coss0  36941  cossid  36942  trcoss  36944  eleccossin  36945  dfssr2  36961  br1cossxrncnvssrres  36970  refsymrels3  37028  refsymrel2  37029  refsymrel3  37030  elrefsymrels3  37032  dfeqvrel2  37052  dfeqvrel3  37053  redundeq1  37091  redundpbi1  37093  dfcomember3  37136  eqvreldmqs  37137  eqvreldmqs2  37138  dfeldisj3  37181  eldisjn0elb  37207  antisymrelres  37225  dfmembpart2  37232  prtlem10  37327  prter1  37341  lcvbr3  37485  isopos  37642  llnexatN  37984  snatpsubN  38213  pclclN  38354  pclfinN  38363  lhpocnel2  38482  cdlemk19w  39435  dih1dimatlem  39792  psspwb  40650  mhphf  40757  mzpclall  41036  mzpincl  41043  mzpindd  41055  2nn0ind  41255  dford4  41339  wopprc  41340  islmodfg  41382  isdomn3  41517  ifpan123g  41721  ifpan23  41722  ifpnot23  41740  ifpdfxor  41749  ifpidg  41753  ifpid1g  41756  ifpim23g  41757  ifpim123g  41762  ifpim1g  41763  ifp1bi  41764  ifpimimb  41766  ifpororb  41767  ifpor123g  41770  ifpbibib  41772  rp-isfinite6  41780  alephiso2  41820  undmrnresiss  41866  cotrintab  41876  brtrclfv2  41989  dfxor4  42028  snhesn  42048  dffrege76  42201  uneqsn  42287  expandan  42558  ismnuprim  42564  nzin  42588  onfrALTlem5  42814  onfrALTlem4  42815  undif3VD  43154  onfrALTlem5VD  43157  onfrALTlem4VD  43158  ndisj2  43249  rexabsle  43644  ellimcabssub0  43848  limsupre2mpt  43961  limsupre3  43964  limsupre3mpt  43965  limsupre3uz  43967  limsupreuz  43968  liminfreuz  44034  fourierdlem103  44440  fourierdlem104  44441  fourierdlem112  44449  smflim  45008  smflim2  45037  smflimsuplem1  45051  smflimsup  45059  cfsetsnfsetf1  45283  2reu8i  45335  ichan  45637  issubmgm  46073  rabsubmgmd  46075  2zlidl  46222  mndpsuppss  46437  islininds2  46555  zlmodzxzldeplem3  46573  2itscp  46857  reutruALT  46881  alsi-no-surprise  47233
  Copyright terms: Public domain W3C validator