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  2338  sbnf2  2363  cbveuvw  2606  cbveuw  2607  cbveuALT  2609  2mo2  2648  2eu4  2656  sbabel  2932  neanior  3026  r19.26m  3097  reeanlem  3209  rexeqbii  3311  reu5  3345  cbvreuw  3369  cgsex4g  3477  reu2  3672  reu3  3674  2reu5a  3691  2reu5lem3  3704  2reu1  3836  eqss  3938  unss  4131  ralunb  4138  ssin  4180  undi  4226  indifdi  4235  undif3  4241  inab  4250  difab  4251  reuss2  4267  reupick  4270  2reu4lem  4464  reuprg  4648  sstp  4780  tpss  4781  prneimg  4798  prneimg2  4799  prnebg  4800  uniin  4875  intun  4923  disjiun  5074  disjxiun  5083  brin  5138  brdif  5139  ssext  5402  pweqb  5404  opthg2  5428  copsex4g  5444  propeqop  5456  eqopab2bw  5497  eqopab2b  5501  pwin  5516  pofun  5551  dffr6  5581  wetrep  5618  elxp3  5691  soinxp  5707  weinxp  5710  csbxp  5726  relun  5761  inopab  5779  difopab  5780  inxp  5781  inxpOLD  5782  opelco2g  5817  cnvco  5835  dmin  5861  restidsing  6013  intasym  6073  asymref  6074  asymref2  6075  cnvdif  6102  xpnz  6118  difxp  6123  xpdifid  6127  xp11  6134  dfco2  6204  cnvpo  6246  cnvso  6247  xpco  6248  reu3op  6251  dfpo2  6255  dffun4  6506  funun  6539  fun11  6567  fununi  6568  imadif  6577  fnres  6620  mptfnf  6628  fnopabg  6630  fun  6697  fin  6715  dff1o2  6780  brprcneu  6825  brprcneuALT  6826  dffv2  6930  fsn  7083  f13dfv  7223  dff1o6  7224  isotr  7285  eqoprab2bw  7431  eqoprab2b  7432  fvmpopr2d  7523  porpss  7675  epweon  7723  onsucb  7762  resf1extb  7879  elxp6  7970  dfoprab3  8001  opiota  8006  poxp  8072  soxp  8073  poxp2  8087  xpord2pred  8089  xpord2indlem  8091  xpord3pred  8096  xpord3inddlem  8098  soseq  8103  suppvalbr  8108  brtpos2  8176  frrlem9  8238  fprlem1  8244  tfrlem7  8316  dfer2  8638  eqer  8674  iiner  8730  uniinqs  8738  brecop  8751  eroveu  8753  erovlem  8754  fsetexb  8805  mapval2  8814  ixpin  8865  boxriin  8882  brsdom  8915  xpcomco  8999  xpassen  9003  sbthlem9  9027  sbthlem10  9028  brsdom2  9033  ssenen  9083  sbthfilem  9126  dffi3  9338  dfsup2  9351  infcllem  9395  axinf2  9555  zfinf2  9557  oemapso  9597  ttrcltr  9631  frrlem15  9675  scottexs  9805  scott0s  9806  kardex  9812  karden  9813  dfac5lem1  10039  dfac5lem3  10041  kmlem15  10081  enfin2i  10237  fin23lem34  10262  brdom7disj  10447  fpwwe2lem11  10558  fpwwe2lem12  10559  axgroth5  10741  grothprim  10751  addsrpr  10992  mulsrpr  10993  mulgt0sr  11022  addcnsr  11052  mulcnsr  11053  ltresr  11057  axcnre  11081  ssxr  11209  infrenegsup  12133  nnwos  12859  zmin  12888  xrnemnf  13062  xrnepnf  13063  xmullem  13210  xmulcom  13212  xmulneg1  13215  xmulf  13218  xrinfmss2  13257  elfzuzb  13466  fzass4  13510  seqof  14015  hashbclem  14408  hashfacen  14410  xpcogend  14930  trclublem  14951  rexanre  15303  caubnd  15315  o1lo1  15493  rpnnen2lem12  16186  lcmcllem  16559  lcmftp  16599  lcmfunsnlem2  16603  isprm3  16646  prmreclem2  16882  4sqlem12  16921  catcone0  17647  isffth2  17879  fucinv  17937  lublecllem  18318  odulub  18365  oduglb  18367  issubmgm  18664  rabsubmgmd  18666  mndpsuppss  18727  issubm  18765  issubmd  18768  0subm  18779  insubm  18780  sursubmefmnd  18858  injsubmefmnd  18859  smndex1mgm  18872  isnsg2  19125  cycsubm  19171  oppgid  19325  symgfixf1  19406  pmtrrn2  19429  lsmdisjr  19653  lsmhash  19674  gsumcom3  19947  dprd0  20002  issrg  20163  dvdsrtr  20342  isirred2  20395  isdomn3  20686  opprdomnb  20688  isdomn4r  20690  lss1d  20952  lspsolvlem  21135  lbsextlem2  21152  cnfldfun  21361  cnfldfunOLD  21374  unocv  21673  iunocv  21674  evlsval  22077  mpomatmul  22424  cpmidpmat  22851  tgval2  22934  fctop  22982  ppttop  22985  epttop  22987  cnnei  23260  2ndcctbss  23433  txuni2  23543  txbas  23545  ptbasin  23555  txdis1cn  23613  xkococnlem  23637  opnfbas  23820  fgcl  23856  fbasrn  23862  filuni  23863  cfinfil  23871  csdfil  23872  fin1aufil  23910  rnelfmlem  23930  fmfnfmlem3  23934  txflf  23984  xmeterval  24410  reconn  24807  iimulcl  24917  isclmp  25077  iscau3  25258  rrxmvallem  25384  minveclem3  25409  pmltpc  25430  ovolfcl  25446  ismbl  25506  dyaddisj  25576  iblre  25774  plyun0  26175  logfaclbnd  27202  lgslem3  27279  lgsdir2lem5  27309  nosupinfsep  27713  ltsrec  27810  madebdaylemlrcut  27908  addsproplem2  27979  addsuniflem  28010  negsproplem2  28038  negsid  28050  mulsproplem5  28129  mulsproplem6  28130  mulsproplem7  28131  mulsproplem8  28132  mulsproplem9  28133  mulsuniflem  28158  precsexlem9  28224  precsexlem10  28225  ons2ind  28284  nnaddscl  28355  nnmulscl  28356  zaddscl  28403  zsoring  28418  recut  28503  readdscl  28508  remulscl  28511  tgjustf  28558  ishpg  28844  usgrexmpllem  29346  nb3grpr2  29469  vtxd0nedgb  29575  wlk1walk  29725  clwlkcompbp  29868  wwlknllvtx  29932  wwlksonvtx  29941  wspthnonp  29945  wwlksn0s  29947  wwlksnndef  29991  2wlkdlem8  30019  elwwlks2s3  30037  clwwlkf1  30137  clwwlknonccat  30184  clwwlknon2x  30191  3pthdlem1  30252  upgr4cycl4dv4e  30273  frgr2wwlk1  30417  frgrreg  30482  ajfval  30898  issh  31297  chcon2i  31553  chcon3i  31555  spanuni  31633  5oalem7  31749  3oalem3  31753  pjin2i  32282  pjin3i  32283  cvnbtwn4  32378  mdslj1i  32408  mdslj2i  32409  mdslmd1i  32418  chrelat4i  32462  chirredi  32483  cdj3i  32530  rmoun  32581  difrab2  32585  eqdif  32607  inpr0  32620  iuninc  32648  fcoinvbr  32693  suppss2f  32729  fmptdF  32747  disjdsct  32794  f1od2  32810  hashxpe  32898  tosglblem  33052  mgcval  33065  pmtrprfv2  33167  elrgspnlem2  33322  ssdifidllem  33534  ssmxidllem  33551  ccfldextdgrr  33835  fldext2chn  33891  ordtconnlem1  34087  esumpfinvalf  34239  esum2dlem  34255  measiuns  34380  eulerpartlemt0  34532  eulerpartlemr  34537  eulerpartlemn  34544  ballotlem2  34652  ballotlemodife  34661  bnj887  34927  bnj976  34939  bnj1385  34993  bnj153  35041  bnj543  35054  bnj607  35077  bnj882  35087  bnj916  35094  bnj983  35112  axreg  35290  axregscl  35291  axregs  35302  derangenlem  35372  pconnconn  35432  fmlaomn0  35591  fmla0disjsuc  35599  fmlasucdisj  35600  elmpst  35737  xpab  35927  dftr6  35952  dffr5  35955  fundmpss  35968  elpotr  35980  brtxp  36079  brpprod  36084  brsset  36088  idsset  36089  dfon3  36091  ellimits  36109  dffun10  36113  elfuns  36114  brcart  36131  brimg  36136  brapply  36137  brcap  36139  lemsuccf  36140  funpartfun  36144  dfrecs2  36151  dfrdg4  36152  altopthc  36172  altopthd  36173  altopelaltxp  36177  outsideoftr  36330  rmoeqbii  36389  reueqbii  36391  rabeqbii  36395  riotaeqbii  36399  ixpeq1i  36401  cbvixpvw2  36446  cbvprodvw2  36448  trer  36517  neibastop1  36560  neifg  36572  df3nandALT1  36600  imnand2  36603  axtco  36672  regsfromregtco  36739  regsfromunir1  36741  mh-prprimbi  36744  eliminable-abelab  37196  bj-eldiag2  37510  bj-imdiridlem  37518  bj-opabco  37521  bj-xpcossxp  37522  topdifinfeq  37683  relowlssretop  37696  relowlpssretop  37697  wl-cases2-dnf  37854  poimirlem30  37988  poimirlem32  37990  ismblfin  37999  mbfposadd  38005  inixp  38066  elghomOLD  38225  keridl  38370  smprngopr  38390  sbcani  38446  inxpxrn  38756  dfcoss2  38841  cosscnv  38844  coss1cnvres  38845  coss2cnvepres  38846  1cossres  38857  dfcoels  38858  trressn  38873  br1cossinres  38875  br1cossinidres  38877  br1cossincnvepres  38878  br1cossxrnidres  38879  br1cossxrncnvepres  38880  cosscnvssid3  38904  coss0  38907  cossid  38908  trcoss  38910  eleccossin  38911  dfssr2  38917  br1cossxrncnvssrres  38926  refsymrels3  38988  refsymrel2  38989  refsymrel3  38990  elrefsymrels3  38992  dfeqvrel2  39012  dfeqvrel3  39013  redundeq1  39051  redundpbi1  39053  dfcomember3  39097  eqvreldmqs  39098  eqvreldmqs2  39099  dfeldisj3  39149  eldisjdmqsim  39155  eldisjn0elb  39183  antisymrelres  39204  dfmembpart2  39211  prtlem10  39328  prter1  39342  lcvbr3  39486  isopos  39643  llnexatN  39984  snatpsubN  40213  pclclN  40354  pclfinN  40363  lhpocnel2  40482  cdlemk19w  41435  dih1dimatlem  41792  psspwb  42686  redvmptabs  42809  mzpclall  43176  mzpincl  43183  mzpindd  43195  2nn0ind  43394  dford4  43478  wopprc  43479  islmodfg  43518  ifpan123g  43907  ifpan23  43908  ifpnot23  43926  ifpdfxor  43935  ifpidg  43939  ifpid1g  43942  ifpim23g  43943  ifpim123g  43948  ifpim1g  43949  ifp1bi  43950  ifpimimb  43952  ifpororb  43953  ifpor123g  43956  ifpbibib  43958  rp-isfinite6  43966  alephiso2  44006  undmrnresiss  44052  cotrintab  44062  brtrclfv2  44175  dfxor4  44214  snhesn  44234  dffrege76  44387  uneqsn  44473  expandan  44736  ismnuprim  44742  nzin  44766  onfrALTlem5  44990  onfrALTlem4  44991  undif3VD  45329  onfrALTlem5VD  45332  onfrALTlem4VD  45333  dfac5prim  45438  wfaxpr  45446  brpermmodel  45451  permac8prim  45462  ndisj2  45503  rexabsle  45868  ellimcabssub0  46068  limsupre2mpt  46179  limsupre3  46182  limsupre3mpt  46183  limsupre3uz  46185  limsupreuz  46186  liminfreuz  46252  fourierdlem103  46658  fourierdlem104  46659  fourierdlem112  46667  smflim  47226  smflim2  47255  smflimsuplem1  47269  smflimsup  47277  cfsetsnfsetf1  47522  2reu8i  47576  ichan  47930  clnbgrsym  48329  dfnbgr6  48348  upgrimpthslem2  48399  isgrlim  48473  usgrexmpl2trifr  48528  pgnbgreunbgrlem5  48614  pgnbgreunbgr  48616  2zlidl  48731  islininds2  48975  zlmodzxzldeplem3  48993  2itscp  49272  reutruALT  49295  iinxp  49321  0funclem  49576  fucofulem2  49801  fuco2el  49802  catcinv  49889  2arwcatlem1  50085  alsi-no-surprise  50286