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

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

Syntax hints:   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  anbi12ci  627  an2anr  634  ordi  1003  ordir  1004  orddi  1007  pm5.17  1009  xor  1012  cases2  1045  3anbi123i  1152  an6  1442  nanbi  1494  cadan  1603  nic-axALT  1669  19.43OLD  1879  sbbi  2298  aaan  2322  sbnf2  2349  eubii  2574  cbveuvw  2594  cbveuw  2595  cbveuALT  2597  2mo2  2636  2eu4  2644  sbabel  2928  sbabelOLD  2929  neanior  3025  r19.26m  3100  reeanlem  3216  2ralorOLD  3220  rexeqbii  3329  reu5  3366  cbvreuw  3394  cgsex4g  3511  reu2  3719  reu3  3721  2reu5a  3738  2reu5lem3  3751  2reu1  3890  eqss  3995  unss  4185  ralunb  4192  ssin  4232  undi  4276  indifdi  4285  indifdirOLD  4287  undif3  4292  inab  4301  difab  4302  reuss2  4318  reupick  4321  2reu4lem  4530  reuprg  4712  sstp  4845  tpss  4846  prneimg  4863  prnebg  4864  uniin  4941  intun  4990  intprOLD  4993  disjiun  5142  disjxiun  5152  brin  5207  brdif  5208  ssext  5462  pweqb  5464  opthg2  5487  copsex4g  5503  propeqop  5515  eqopab2bw  5556  eqopab2b  5560  pwin  5578  pofun  5614  dffr6  5642  wetrep  5677  elxp3  5750  soinxp  5765  weinxp  5768  csbxp  5783  relun  5819  inopab  5837  difopab  5838  difopabOLD  5839  inxp  5840  inxpOLD  5841  opelco2g  5876  cnvco  5894  dmin  5920  restidsing  6064  intasym  6129  asymref  6130  asymref2  6131  cnvdif  6157  xpnz  6172  difxp  6177  xpdifid  6181  xp11  6188  dfco2  6258  relssdmrnOLD  6282  cnvpo  6300  cnvso  6301  xpco  6302  reu3op  6305  dfpo2  6309  dffun4  6572  funun  6607  fun11  6635  fununi  6636  imadif  6645  fnres  6690  mptfnf  6698  fnopabg  6700  fun  6766  fin  6784  dff1o2  6850  brprcneu  6893  brprcneuALT  6894  dffv2  6999  fsn  7151  f13dfv  7290  dff1o6  7291  isotr  7350  eqoprab2bw  7497  eqoprab2b  7498  fvmpopr2d  7590  porpss  7740  epweon  7785  onsucb  7828  elxp6  8039  dfoprab3  8070  opiota  8075  poxp  8144  soxp  8145  poxp2  8159  xpord2pred  8161  xpord2indlem  8163  xpord3pred  8168  xpord3inddlem  8170  soseq  8175  suppvalbr  8180  brtpos2  8249  frrlem9  8311  fprlem1  8317  wfrlem5OLD  8345  wfrfunOLD  8351  tfrlem7  8415  dfer2  8737  eqer  8772  iiner  8820  uniinqs  8828  brecop  8841  eroveu  8843  erovlem  8844  fsetexb  8895  mapval2  8903  ixpin  8954  boxriin  8971  brsdom  9008  xpcomco  9102  xpassen  9106  sbthlem9  9131  sbthlem10  9132  brsdom2  9137  ssenen  9191  sbthfilem  9237  unfiOLD  9349  dffi3  9476  dfsup2  9489  infcllem  9532  axinf2  9685  zfinf2  9687  oemapso  9727  ttrcltr  9761  frrlem15  9802  scottexs  9932  scott0s  9933  kardex  9939  karden  9940  dfac5lem1  10168  dfac5lem3  10170  kmlem15  10209  enfin2i  10366  fin23lem34  10391  brdom7disj  10576  fpwwe2lem11  10686  fpwwe2lem12  10687  axgroth5  10869  grothprim  10879  addsrpr  11120  mulsrpr  11121  mulgt0sr  11150  addcnsr  11180  mulcnsr  11181  ltresr  11185  axcnre  11209  1re  11266  ssxr  11335  infrenegsup  12251  nnwos  12953  zmin  12982  xrnemnf  13153  xrnepnf  13154  xmullem  13299  xmulcom  13301  xmulneg1  13304  xmulf  13307  xrinfmss2  13346  elfzuzb  13551  fzass4  13595  seqof  14081  hashbclem  14471  hashfacen  14473  hashfacenOLD  14474  xpcogend  14981  trclublem  15002  rexanre  15353  caubnd  15365  o1lo1  15541  rpnnen2lem12  16229  lcmcllem  16599  lcmftp  16639  lcmfunsnlem2  16643  isprm3  16686  prmreclem2  16921  4sqlem12  16960  catcone0  17702  isffth2  17940  fucinv  18000  lublecllem  18387  odulub  18434  oduglb  18436  issubmgm  18697  rabsubmgmd  18699  issubm  18795  issubmd  18798  0subm  18809  insubm  18810  sursubmefmnd  18888  injsubmefmnd  18889  smndex1mgm  18899  isnsg2  19152  cycsubm  19198  oppgid  19355  symgfixf1  19437  pmtrrn2  19460  lsmdisjr  19684  lsmhash  19705  gsumcom3  19978  dprd0  20033  issrg  20173  dvdsrtr  20352  isirred2  20405  isdomn3  20695  opprdomnb  20697  isdomn4r  20699  lss1d  20942  lspsolvlem  21125  lbsextlem2  21142  cnfldfun  21359  cnfldfunOLD  21372  unocv  21678  iunocv  21679  evlsval  22103  mpomatmul  22442  cpmidpmat  22869  tgval2  22953  fctop  23001  ppttop  23004  epttop  23006  cnnei  23280  2ndcctbss  23453  txuni2  23563  txbas  23565  ptbasin  23575  txdis1cn  23633  xkococnlem  23657  opnfbas  23840  fgcl  23876  fbasrn  23882  filuni  23883  cfinfil  23891  csdfil  23892  fin1aufil  23930  rnelfmlem  23950  fmfnfmlem3  23954  txflf  24004  xmeterval  24432  reconn  24838  iimulcl  24954  isclmp  25118  iscau3  25300  rrxmvallem  25426  minveclem3  25451  pmltpc  25473  ovolfcl  25489  ismbl  25549  dyaddisj  25619  iblre  25817  plyun0  26227  logfaclbnd  27254  lgslem3  27331  lgsdir2lem5  27361  nosupinfsep  27765  nocvxmin  27811  sltrec  27853  madebdaylemlrcut  27925  addsproplem2  27987  addsuniflem  28018  negsproplem2  28041  negsid  28053  mulsproplem5  28124  mulsproplem6  28125  mulsproplem7  28126  mulsproplem8  28127  mulsproplem9  28128  mulsuniflem  28153  precsexlem9  28217  precsexlem10  28218  nnaddscl  28318  nnmulscl  28319  recut  28350  0reno  28351  readdscl  28353  remulscl  28356  tgjustf  28403  ishpg  28689  usgrexmpllem  29199  nb3grpr2  29322  vtxd0nedgb  29428  wlk1walk  29579  clwlkcompbp  29722  wwlknllvtx  29783  wwlksonvtx  29792  wspthnonp  29796  wwlksn0s  29798  wwlksnndef  29842  2wlkdlem8  29870  elwwlks2s3  29888  clwwlkf1  29985  clwwlknonccat  30032  clwwlknon2x  30039  3pthdlem1  30100  upgr4cycl4dv4e  30121  frgr2wwlk1  30265  frgrreg  30330  ajfval  30745  issh  31144  chcon2i  31400  chcon3i  31402  spanuni  31480  5oalem7  31596  3oalem3  31600  pjin2i  32129  pjin3i  32130  cvnbtwn4  32225  mdslj1i  32255  mdslj2i  32256  mdslmd1i  32265  chrelat4i  32309  chirredi  32330  cdj3i  32377  rmoun  32425  difrab2  32429  eqdif  32449  inpr0  32460  iuninc  32483  fcoinvbr  32527  suppss2f  32557  fmptdF  32575  disjdsct  32616  cnvoprabOLD  32636  f1od2  32637  hashxpe  32713  tosglblem  32846  mgcval  32859  pmtrprfv2  32968  ssdifidllem  33333  ssmxidllem  33350  ccfldextdgrr  33560  ordtconnlem1  33741  esumpfinvalf  33911  esum2dlem  33927  measiuns  34052  eulerpartlemt0  34205  eulerpartlemr  34210  eulerpartlemn  34217  ballotlem2  34324  ballotlemodife  34333  bnj887  34612  bnj976  34624  bnj1385  34679  bnj153  34727  bnj543  34740  bnj607  34763  bnj882  34773  bnj916  34780  bnj983  34798  derangenlem  35001  pconnconn  35061  fmlaomn0  35220  fmla0disjsuc  35228  fmlasucdisj  35229  elmpst  35366  xpab  35550  dftr6  35575  dffr5  35578  fundmpss  35592  elpotr  35607  brtxp  35706  brpprod  35711  brsset  35715  idsset  35716  dfon3  35718  ellimits  35736  dffun10  35740  elfuns  35741  brcart  35758  brimg  35763  brapply  35764  brcap  35766  brsuccf  35767  funpartfun  35769  dfrecs2  35776  dfrdg4  35777  altopthc  35797  altopthd  35798  altopelaltxp  35802  outsideoftr  35955  trer  36030  neibastop1  36073  neifg  36085  df3nandALT1  36113  imnand2  36116  eliminable-abelab  36577  bj-eldiag2  36886  bj-imdiridlem  36894  bj-opabco  36897  bj-xpcossxp  36898  topdifinfeq  37059  relowlssretop  37072  relowlpssretop  37073  wl-cases2-dnf  37209  poimirlem30  37353  poimirlem32  37355  ismblfin  37364  mbfposadd  37370  inixp  37431  elghomOLD  37590  keridl  37735  smprngopr  37755  sbcani  37811  inxpxrn  38095  dfcoss2  38113  cosscnv  38116  coss1cnvres  38117  coss2cnvepres  38118  1cossres  38129  dfcoels  38130  trressn  38145  br1cossinres  38147  br1cossinidres  38149  br1cossincnvepres  38150  br1cossxrnidres  38151  br1cossxrncnvepres  38152  cosscnvssid3  38176  coss0  38179  cossid  38180  trcoss  38182  eleccossin  38183  dfssr2  38199  br1cossxrncnvssrres  38208  refsymrels3  38266  refsymrel2  38267  refsymrel3  38268  elrefsymrels3  38270  dfeqvrel2  38290  dfeqvrel3  38291  redundeq1  38329  redundpbi1  38331  dfcomember3  38374  eqvreldmqs  38375  eqvreldmqs2  38376  dfeldisj3  38419  eldisjn0elb  38445  antisymrelres  38463  dfmembpart2  38470  prtlem10  38565  prter1  38579  lcvbr3  38723  isopos  38880  llnexatN  39222  snatpsubN  39451  pclclN  39592  pclfinN  39601  lhpocnel2  39720  cdlemk19w  40673  dih1dimatlem  41030  psspwb  41952  mzpclall  42402  mzpincl  42409  mzpindd  42421  2nn0ind  42621  dford4  42705  wopprc  42706  islmodfg  42748  ifpan123g  43144  ifpan23  43145  ifpnot23  43163  ifpdfxor  43172  ifpidg  43176  ifpid1g  43179  ifpim23g  43180  ifpim123g  43185  ifpim1g  43186  ifp1bi  43187  ifpimimb  43189  ifpororb  43190  ifpor123g  43193  ifpbibib  43195  rp-isfinite6  43203  alephiso2  43243  undmrnresiss  43289  cotrintab  43299  brtrclfv2  43412  dfxor4  43451  snhesn  43471  dffrege76  43624  uneqsn  43710  expandan  43980  ismnuprim  43986  nzin  44010  onfrALTlem5  44236  onfrALTlem4  44237  undif3VD  44576  onfrALTlem5VD  44579  onfrALTlem4VD  44580  ndisj2  44670  rexabsle  45052  ellimcabssub0  45256  limsupre2mpt  45369  limsupre3  45372  limsupre3mpt  45373  limsupre3uz  45375  limsupreuz  45376  liminfreuz  45442  fourierdlem103  45848  fourierdlem104  45849  fourierdlem112  45857  smflim  46416  smflim2  46445  smflimsuplem1  46459  smflimsup  46467  cfsetsnfsetf1  46692  2reu8i  46744  ichan  47045  clnbgrsym  47426  dfnbgr6  47442  gricer  47490  isgrlim  47506  2zlidl  47635  mndpsuppss  47768  islininds2  47885  zlmodzxzldeplem3  47903  2itscp  48187  reutruALT  48210  alsi-no-surprise  48562