Theorem anbi12i 629

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

Step	Hyp	Ref	Expression
1		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
2	1	anbi2i 624	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜃))
3		anbi12.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	bianbi 628	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anbi12ci  630  an2anr  637  ordi  1008  ordir  1009  orddi  1012  pm5.17  1014  xor  1017  cases2  1048  3anbi123i  1156  an6  1448  nanbi  1502  cadan  1611  nic-axALT  1676  19.43OLD  1885  sbbi  2314  aaan  2337  sbnf2  2362  cbveuvw  2605  cbveuw  2606  cbveuALT  2608  2mo2  2647  2eu4  2655  sbabel  2931  neanior  3025  r19.26m  3096  reeanlem  3208  rexeqbii  3310  reu5  3344  cbvreuw  3368  cgsex4g  3476  reu2  3671  reu3  3673  2reu5a  3690  2reu5lem3  3703  2reu1  3835  eqss  3937  unss  4130  ralunb  4137  ssin  4179  undi  4225  indifdi  4234  undif3  4240  inab  4249  difab  4250  reuss2  4266  reupick  4269  2reu4lem  4463  reuprg  4647  sstp  4779  tpss  4780  prneimg  4797  prneimg2  4798  prnebg  4799  uniin  4874  intun  4922  disjiun  5073  disjxiun  5082  brin  5137  brdif  5138  ssext  5406  pweqb  5408  opthg2  5432  copsex4g  5449  propeqop  5461  eqopab2bw  5503  eqopab2b  5507  pwin  5522  pofun  5557  dffr6  5587  wetrep  5624  elxp3  5697  soinxp  5713  weinxp  5716  csbxp  5732  relun  5767  inopab  5785  difopab  5786  inxp  5787  opelco2g  5822  cnvco  5840  dmin  5866  restidsing  6018  intasym  6078  asymref  6079  asymref2  6080  cnvdif  6107  xpnz  6123  difxp  6128  xpdifid  6132  xp11  6139  dfco2  6209  cnvpo  6251  cnvso  6252  xpco  6253  reu3op  6256  dfpo2  6260  dffun4  6511  funun  6544  fun11  6572  fununi  6573  imadif  6582  fnres  6625  mptfnf  6633  fnopabg  6635  fun  6702  fin  6720  dff1o2  6785  brprcneu  6830  brprcneuALT  6831  dffv2  6935  fsn  7088  f13dfv  7229  dff1o6  7230  isotr  7291  eqoprab2bw  7437  eqoprab2b  7438  fvmpopr2d  7529  porpss  7681  epweon  7729  onsucb  7768  resf1extb  7885  elxp6  7976  dfoprab3  8007  opiota  8012  poxp  8078  soxp  8079  poxp2  8093  xpord2pred  8095  xpord2indlem  8097  xpord3pred  8102  xpord3inddlem  8104  soseq  8109  suppvalbr  8114  brtpos2  8182  frrlem9  8244  fprlem1  8250  tfrlem7  8322  dfer2  8644  eqer  8680  iiner  8736  uniinqs  8744  brecop  8757  eroveu  8759  erovlem  8760  fsetexb  8811  mapval2  8820  ixpin  8871  boxriin  8888  brsdom  8921  xpcomco  9005  xpassen  9009  sbthlem9  9033  sbthlem10  9034  brsdom2  9039  ssenen  9089  sbthfilem  9132  dffi3  9344  dfsup2  9357  infcllem  9401  axinf2  9561  zfinf2  9563  oemapso  9603  ttrcltr  9637  frrlem15  9681  scottexs  9811  scott0s  9812  kardex  9818  karden  9819  dfac5lem1  10045  dfac5lem3  10047  kmlem15  10087  enfin2i  10243  fin23lem34  10268  brdom7disj  10453  fpwwe2lem11  10564  fpwwe2lem12  10565  axgroth5  10747  grothprim  10757  addsrpr  10998  mulsrpr  10999  mulgt0sr  11028  addcnsr  11058  mulcnsr  11059  ltresr  11063  axcnre  11087  ssxr  11215  infrenegsup  12139  nnwos  12865  zmin  12894  xrnemnf  13068  xrnepnf  13069  xmullem  13216  xmulcom  13218  xmulneg1  13221  xmulf  13224  xrinfmss2  13263  elfzuzb  13472  fzass4  13516  seqof  14021  hashbclem  14414  hashfacen  14416  xpcogend  14936  trclublem  14957  rexanre  15309  caubnd  15321  o1lo1  15499  rpnnen2lem12  16192  lcmcllem  16565  lcmftp  16605  lcmfunsnlem2  16609  isprm3  16652  prmreclem2  16888  4sqlem12  16927  catcone0  17653  isffth2  17885  fucinv  17943  lublecllem  18324  odulub  18371  oduglb  18373  issubmgm  18670  rabsubmgmd  18672  mndpsuppss  18733  issubm  18771  issubmd  18774  0subm  18785  insubm  18786  sursubmefmnd  18864  injsubmefmnd  18865  smndex1mgm  18878  isnsg2  19131  cycsubm  19177  oppgid  19331  symgfixf1  19412  pmtrrn2  19435  lsmdisjr  19659  lsmhash  19680  gsumcom3  19953  dprd0  20008  issrg  20169  dvdsrtr  20348  isirred2  20401  isdomn3  20692  opprdomnb  20694  isdomn4r  20696  lss1d  20958  lspsolvlem  21140  lbsextlem2  21157  cnfldfun  21366  unocv  21660  iunocv  21661  evlsval  22064  mpomatmul  22411  cpmidpmat  22838  tgval2  22921  fctop  22969  ppttop  22972  epttop  22974  cnnei  23247  2ndcctbss  23420  txuni2  23530  txbas  23532  ptbasin  23542  txdis1cn  23600  xkococnlem  23624  opnfbas  23807  fgcl  23843  fbasrn  23849  filuni  23850  cfinfil  23858  csdfil  23859  fin1aufil  23897  rnelfmlem  23917  fmfnfmlem3  23921  txflf  23971  xmeterval  24397  reconn  24794  iimulcl  24904  isclmp  25064  iscau3  25245  rrxmvallem  25371  minveclem3  25396  pmltpc  25417  ovolfcl  25433  ismbl  25493  dyaddisj  25563  iblre  25761  plyun0  26162  logfaclbnd  27185  lgslem3  27262  lgsdir2lem5  27292  nosupinfsep  27696  ltsrec  27793  madebdaylemlrcut  27891  addsproplem2  27962  addsuniflem  27993  negsproplem2  28021  negsid  28033  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  mulsproplem9  28116  mulsuniflem  28141  precsexlem9  28207  precsexlem10  28208  ons2ind  28267  nnaddscl  28338  nnmulscl  28339  zaddscl  28386  zsoring  28401  recut  28486  readdscl  28491  remulscl  28494  tgjustf  28541  ishpg  28827  usgrexmpllem  29329  nb3grpr2  29452  vtxd0nedgb  29557  wlk1walk  29707  clwlkcompbp  29850  wwlknllvtx  29914  wwlksonvtx  29923  wspthnonp  29927  wwlksn0s  29929  wwlksnndef  29973  2wlkdlem8  30001  elwwlks2s3  30019  clwwlkf1  30119  clwwlknonccat  30166  clwwlknon2x  30173  3pthdlem1  30234  upgr4cycl4dv4e  30255  frgr2wwlk1  30399  frgrreg  30464  ajfval  30880  issh  31279  chcon2i  31535  chcon3i  31537  spanuni  31615  5oalem7  31731  3oalem3  31735  pjin2i  32264  pjin3i  32265  cvnbtwn4  32360  mdslj1i  32390  mdslj2i  32391  mdslmd1i  32400  chrelat4i  32444  chirredi  32465  cdj3i  32512  rmoun  32563  difrab2  32567  eqdif  32589  inpr0  32602  iuninc  32630  fcoinvbr  32675  suppss2f  32711  fmptdF  32729  disjdsct  32776  f1od2  32792  hashxpe  32880  tosglblem  33034  mgcval  33047  pmtrprfv2  33149  elrgspnlem2  33304  ssdifidllem  33516  ssmxidllem  33533  ccfldextdgrr  33816  fldext2chn  33872  ordtconnlem1  34068  esumpfinvalf  34220  esum2dlem  34236  measiuns  34361  eulerpartlemt0  34513  eulerpartlemr  34518  eulerpartlemn  34525  ballotlem2  34633  ballotlemodife  34642  bnj887  34908  bnj976  34920  bnj1385  34974  bnj153  35022  bnj543  35035  bnj607  35058  bnj882  35068  bnj916  35075  bnj983  35093  axreg  35271  axregscl  35272  axregs  35283  derangenlem  35353  pconnconn  35413  fmlaomn0  35572  fmla0disjsuc  35580  fmlasucdisj  35581  elmpst  35718  xpab  35908  dftr6  35933  dffr5  35936  fundmpss  35949  elpotr  35961  brtxp  36060  brpprod  36065  brsset  36069  idsset  36070  dfon3  36072  ellimits  36090  dffun10  36094  elfuns  36095  brcart  36112  brimg  36117  brapply  36118  brcap  36120  lemsuccf  36121  funpartfun  36125  dfrecs2  36132  dfrdg4  36133  altopthc  36153  altopthd  36154  altopelaltxp  36158  outsideoftr  36311  rmoeqbii  36370  reueqbii  36372  rabeqbii  36376  riotaeqbii  36380  ixpeq1i  36382  cbvixpvw2  36427  cbvprodvw2  36429  trer  36498  neibastop1  36541  neifg  36553  df3nandALT1  36581  imnand2  36584  axtco  36653  regsfromregtco  36720  regsfromunir1  36722  mh-prprimbi  36725  eliminable-abelab  37177  bj-eldiag2  37491  bj-imdiridlem  37499  bj-opabco  37502  bj-xpcossxp  37503  topdifinfeq  37666  relowlssretop  37679  relowlpssretop  37680  wl-cases2-dnf  37837  poimirlem30  37971  poimirlem32  37973  ismblfin  37982  mbfposadd  37988  inixp  38049  elghomOLD  38208  keridl  38353  smprngopr  38373  sbcani  38429  inxpxrn  38739  dfcoss2  38824  cosscnv  38827  coss1cnvres  38828  coss2cnvepres  38829  1cossres  38840  dfcoels  38841  trressn  38856  br1cossinres  38858  br1cossinidres  38860  br1cossincnvepres  38861  br1cossxrnidres  38862  br1cossxrncnvepres  38863  cosscnvssid3  38887  coss0  38890  cossid  38891  trcoss  38893  eleccossin  38894  dfssr2  38900  br1cossxrncnvssrres  38909  refsymrels3  38971  refsymrel2  38972  refsymrel3  38973  elrefsymrels3  38975  dfeqvrel2  38995  dfeqvrel3  38996  redundeq1  39034  redundpbi1  39036  dfcomember3  39080  eqvreldmqs  39081  eqvreldmqs2  39082  dfeldisj3  39132  eldisjdmqsim  39138  eldisjn0elb  39166  antisymrelres  39187  dfmembpart2  39194  prtlem10  39311  prter1  39325  lcvbr3  39469  isopos  39626  llnexatN  39967  snatpsubN  40196  pclclN  40337  pclfinN  40346  lhpocnel2  40465  cdlemk19w  41418  dih1dimatlem  41775  psspwb  42669  redvmptabs  42792  mzpclall  43159  mzpincl  43166  mzpindd  43178  2nn0ind  43373  dford4  43457  wopprc  43458  islmodfg  43497  ifpan123g  43886  ifpan23  43887  ifpnot23  43905  ifpdfxor  43914  ifpidg  43918  ifpid1g  43921  ifpim23g  43922  ifpim123g  43927  ifpim1g  43928  ifp1bi  43929  ifpimimb  43931  ifpororb  43932  ifpor123g  43935  ifpbibib  43937  rp-isfinite6  43945  alephiso2  43985  undmrnresiss  44031  cotrintab  44041  brtrclfv2  44154  dfxor4  44193  snhesn  44213  dffrege76  44366  uneqsn  44452  expandan  44715  ismnuprim  44721  nzin  44745  onfrALTlem5  44969  onfrALTlem4  44970  undif3VD  45308  onfrALTlem5VD  45311  onfrALTlem4VD  45312  dfac5prim  45417  wfaxpr  45425  brpermmodel  45430  permac8prim  45441  ndisj2  45482  rexabsle  45847  ellimcabssub0  46047  limsupre2mpt  46158  limsupre3  46161  limsupre3mpt  46162  limsupre3uz  46164  limsupreuz  46165  liminfreuz  46231  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  smflim  47205  smflim2  47234  smflimsuplem1  47248  smflimsup  47256  cfsetsnfsetf1  47507  2reu8i  47561  ichan  47915  clnbgrsym  48314  dfnbgr6  48333  upgrimpthslem2  48384  isgrlim  48458  usgrexmpl2trifr  48513  pgnbgreunbgrlem5  48599  pgnbgreunbgr  48601  2zlidl  48716  islininds2  48960  zlmodzxzldeplem3  48978  2itscp  49257  reutruALT  49280  iinxp  49306  0funclem  49561  fucofulem2  49786  fuco2el  49787  catcinv  49874  2arwcatlem1  50070  alsi-no-surprise  50271