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

Step	Hyp	Ref	Expression
1		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
2	1	anbi2i 622	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜃))
3		anbi12.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	bianbi 626	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  628  an2anr  635  ordi  1006  ordir  1007  orddi  1010  pm5.17  1012  xor  1015  cases2  1048  3anbi123i  1155  an6  1445  nanbi  1497  cadan  1606  nic-axALT  1672  19.43OLD  1882  sbbi  2312  aaan  2337  sbnf2  2364  eubii  2588  cbveuvw  2608  cbveuw  2609  cbveuALT  2611  2mo2  2650  2eu4  2658  sbabel  2944  sbabelOLD  2945  neanior  3041  r19.26m  3116  reeanlem  3234  2ralorOLD  3238  rexeqbii  3353  reu5  3390  cbvreuw  3418  cgsex4g  3538  reu2  3747  reu3  3749  2reu5a  3766  2reu5lem3  3779  2reu1  3919  eqss  4024  unss  4213  ralunb  4220  ssin  4260  undi  4304  indifdi  4313  undif3  4319  inab  4328  difab  4329  reuss2  4345  reupick  4348  2reu4lem  4545  reuprg  4728  sstp  4861  tpss  4862  prneimg  4879  prnebg  4880  uniin  4955  intun  5004  disjiun  5154  disjxiun  5163  brin  5218  brdif  5219  ssext  5474  pweqb  5476  opthg2  5499  copsex4g  5514  propeqop  5526  eqopab2bw  5567  eqopab2b  5571  pwin  5589  pofun  5626  dffr6  5655  wetrep  5693  elxp3  5766  soinxp  5781  weinxp  5784  csbxp  5799  relun  5835  inopab  5853  difopab  5854  difopabOLD  5855  inxp  5856  inxpOLD  5857  opelco2g  5892  cnvco  5910  dmin  5936  restidsing  6082  intasym  6147  asymref  6148  asymref2  6149  cnvdif  6175  xpnz  6190  difxp  6195  xpdifid  6199  xp11  6206  dfco2  6276  relssdmrnOLD  6300  cnvpo  6318  cnvso  6319  xpco  6320  reu3op  6323  dfpo2  6327  dffun4  6589  funun  6624  fun11  6652  fununi  6653  imadif  6662  fnres  6707  mptfnf  6715  fnopabg  6717  fun  6783  fin  6801  dff1o2  6867  brprcneu  6910  brprcneuALT  6911  dffv2  7017  fsn  7169  f13dfv  7310  dff1o6  7311  isotr  7372  eqoprab2bw  7520  eqoprab2b  7521  fvmpopr2d  7612  porpss  7762  epweon  7810  onsucb  7853  elxp6  8064  dfoprab3  8095  opiota  8100  poxp  8169  soxp  8170  poxp2  8184  xpord2pred  8186  xpord2indlem  8188  xpord3pred  8193  xpord3inddlem  8195  soseq  8200  suppvalbr  8205  brtpos2  8273  frrlem9  8335  fprlem1  8341  wfrlem5OLD  8369  wfrfunOLD  8375  tfrlem7  8439  dfer2  8764  eqer  8799  iiner  8847  uniinqs  8855  brecop  8868  eroveu  8870  erovlem  8871  fsetexb  8922  mapval2  8930  ixpin  8981  boxriin  8998  brsdom  9035  xpcomco  9128  xpassen  9132  sbthlem9  9157  sbthlem10  9158  brsdom2  9163  ssenen  9217  sbthfilem  9264  dffi3  9500  dfsup2  9513  infcllem  9556  axinf2  9709  zfinf2  9711  oemapso  9751  ttrcltr  9785  frrlem15  9826  scottexs  9956  scott0s  9957  kardex  9963  karden  9964  dfac5lem1  10192  dfac5lem3  10194  kmlem15  10234  enfin2i  10390  fin23lem34  10415  brdom7disj  10600  fpwwe2lem11  10710  fpwwe2lem12  10711  axgroth5  10893  grothprim  10903  addsrpr  11144  mulsrpr  11145  mulgt0sr  11174  addcnsr  11204  mulcnsr  11205  ltresr  11209  axcnre  11233  1re  11290  ssxr  11359  infrenegsup  12278  nnwos  12980  zmin  13009  xrnemnf  13180  xrnepnf  13181  xmullem  13326  xmulcom  13328  xmulneg1  13331  xmulf  13334  xrinfmss2  13373  elfzuzb  13578  fzass4  13622  seqof  14110  hashbclem  14501  hashfacen  14503  xpcogend  15023  trclublem  15044  rexanre  15395  caubnd  15407  o1lo1  15583  rpnnen2lem12  16273  lcmcllem  16643  lcmftp  16683  lcmfunsnlem2  16687  isprm3  16730  prmreclem2  16964  4sqlem12  17003  catcone0  17745  isffth2  17983  fucinv  18043  lublecllem  18430  odulub  18477  oduglb  18479  issubmgm  18740  rabsubmgmd  18742  issubm  18838  issubmd  18841  0subm  18852  insubm  18853  sursubmefmnd  18931  injsubmefmnd  18932  smndex1mgm  18942  isnsg2  19196  cycsubm  19242  oppgid  19399  symgfixf1  19479  pmtrrn2  19502  lsmdisjr  19726  lsmhash  19747  gsumcom3  20020  dprd0  20075  issrg  20215  dvdsrtr  20394  isirred2  20447  isdomn3  20737  opprdomnb  20739  isdomn4r  20741  lss1d  20984  lspsolvlem  21167  lbsextlem2  21184  cnfldfun  21401  cnfldfunOLD  21414  unocv  21721  iunocv  21722  evlsval  22133  mpomatmul  22473  cpmidpmat  22900  tgval2  22984  fctop  23032  ppttop  23035  epttop  23037  cnnei  23311  2ndcctbss  23484  txuni2  23594  txbas  23596  ptbasin  23606  txdis1cn  23664  xkococnlem  23688  opnfbas  23871  fgcl  23907  fbasrn  23913  filuni  23914  cfinfil  23922  csdfil  23923  fin1aufil  23961  rnelfmlem  23981  fmfnfmlem3  23985  txflf  24035  xmeterval  24463  reconn  24869  iimulcl  24985  isclmp  25149  iscau3  25331  rrxmvallem  25457  minveclem3  25482  pmltpc  25504  ovolfcl  25520  ismbl  25580  dyaddisj  25650  iblre  25849  plyun0  26256  logfaclbnd  27284  lgslem3  27361  lgsdir2lem5  27391  nosupinfsep  27795  nocvxmin  27841  sltrec  27883  madebdaylemlrcut  27955  addsproplem2  28021  addsuniflem  28052  negsproplem2  28079  negsid  28091  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  mulsproplem9  28168  mulsuniflem  28193  precsexlem9  28257  precsexlem10  28258  nnaddscl  28367  nnmulscl  28368  zaddscl  28398  recut  28446  0reno  28447  readdscl  28449  remulscl  28452  tgjustf  28499  ishpg  28785  usgrexmpllem  29295  nb3grpr2  29418  vtxd0nedgb  29524  wlk1walk  29675  clwlkcompbp  29818  wwlknllvtx  29879  wwlksonvtx  29888  wspthnonp  29892  wwlksn0s  29894  wwlksnndef  29938  2wlkdlem8  29966  elwwlks2s3  29984  clwwlkf1  30081  clwwlknonccat  30128  clwwlknon2x  30135  3pthdlem1  30196  upgr4cycl4dv4e  30217  frgr2wwlk1  30361  frgrreg  30426  ajfval  30841  issh  31240  chcon2i  31496  chcon3i  31498  spanuni  31576  5oalem7  31692  3oalem3  31696  pjin2i  32225  pjin3i  32226  cvnbtwn4  32321  mdslj1i  32351  mdslj2i  32352  mdslmd1i  32361  chrelat4i  32405  chirredi  32426  cdj3i  32473  rmoun  32522  difrab2  32526  eqdif  32549  inpr0  32560  iuninc  32583  fcoinvbr  32627  suppss2f  32657  fmptdF  32674  disjdsct  32714  cnvoprabOLD  32734  f1od2  32735  hashxpe  32814  tosglblem  32947  mgcval  32960  pmtrprfv2  33081  ssdifidllem  33449  ssmxidllem  33466  ccfldextdgrr  33682  ordtconnlem1  33870  esumpfinvalf  34040  esum2dlem  34056  measiuns  34181  eulerpartlemt0  34334  eulerpartlemr  34339  eulerpartlemn  34346  ballotlem2  34453  ballotlemodife  34462  bnj887  34741  bnj976  34753  bnj1385  34808  bnj153  34856  bnj543  34869  bnj607  34892  bnj882  34902  bnj916  34909  bnj983  34927  derangenlem  35139  pconnconn  35199  fmlaomn0  35358  fmla0disjsuc  35366  fmlasucdisj  35367  elmpst  35504  xpab  35688  dftr6  35713  dffr5  35716  fundmpss  35730  elpotr  35745  brtxp  35844  brpprod  35849  brsset  35853  idsset  35854  dfon3  35856  ellimits  35874  dffun10  35878  elfuns  35879  brcart  35896  brimg  35901  brapply  35902  brcap  35904  brsuccf  35905  funpartfun  35907  dfrecs2  35914  dfrdg4  35915  altopthc  35935  altopthd  35936  altopelaltxp  35940  outsideoftr  36093  rmoeqbii  36152  reueqbii  36154  rabeqbii  36158  riotaeqbii  36162  ixpeq1i  36164  cbvixpvw2  36211  cbvprodvw2  36213  trer  36282  neibastop1  36325  neifg  36337  df3nandALT1  36365  imnand2  36368  eliminable-abelab  36836  bj-eldiag2  37143  bj-imdiridlem  37151  bj-opabco  37154  bj-xpcossxp  37155  topdifinfeq  37316  relowlssretop  37329  relowlpssretop  37330  wl-cases2-dnf  37466  poimirlem30  37610  poimirlem32  37612  ismblfin  37621  mbfposadd  37627  inixp  37688  elghomOLD  37847  keridl  37992  smprngopr  38012  sbcani  38068  inxpxrn  38351  dfcoss2  38369  cosscnv  38372  coss1cnvres  38373  coss2cnvepres  38374  1cossres  38385  dfcoels  38386  trressn  38401  br1cossinres  38403  br1cossinidres  38405  br1cossincnvepres  38406  br1cossxrnidres  38407  br1cossxrncnvepres  38408  cosscnvssid3  38432  coss0  38435  cossid  38436  trcoss  38438  eleccossin  38439  dfssr2  38455  br1cossxrncnvssrres  38464  refsymrels3  38522  refsymrel2  38523  refsymrel3  38524  elrefsymrels3  38526  dfeqvrel2  38546  dfeqvrel3  38547  redundeq1  38585  redundpbi1  38587  dfcomember3  38630  eqvreldmqs  38631  eqvreldmqs2  38632  dfeldisj3  38675  eldisjn0elb  38701  antisymrelres  38719  dfmembpart2  38726  prtlem10  38821  prter1  38835  lcvbr3  38979  isopos  39136  llnexatN  39478  snatpsubN  39707  pclclN  39848  pclfinN  39857  lhpocnel2  39976  cdlemk19w  40929  dih1dimatlem  41286  psspwb  42221  mzpclall  42683  mzpincl  42690  mzpindd  42702  2nn0ind  42902  dford4  42986  wopprc  42987  islmodfg  43026  ifpan123g  43421  ifpan23  43422  ifpnot23  43440  ifpdfxor  43449  ifpidg  43453  ifpid1g  43456  ifpim23g  43457  ifpim123g  43462  ifpim1g  43463  ifp1bi  43464  ifpimimb  43466  ifpororb  43467  ifpor123g  43470  ifpbibib  43472  rp-isfinite6  43480  alephiso2  43520  undmrnresiss  43566  cotrintab  43576  brtrclfv2  43689  dfxor4  43728  snhesn  43748  dffrege76  43901  uneqsn  43987  expandan  44257  ismnuprim  44263  nzin  44287  onfrALTlem5  44513  onfrALTlem4  44514  undif3VD  44853  onfrALTlem5VD  44856  onfrALTlem4VD  44857  ndisj2  44953  rexabsle  45334  ellimcabssub0  45538  limsupre2mpt  45651  limsupre3  45654  limsupre3mpt  45655  limsupre3uz  45657  limsupreuz  45658  liminfreuz  45724  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  smflim  46698  smflim2  46727  smflimsuplem1  46741  smflimsup  46749  cfsetsnfsetf1  46974  2reu8i  47028  ichan  47329  clnbgrsym  47710  dfnbgr6  47729  isgrlim  47806  usgrexmpl2trifr  47852  2zlidl  47963  mndpsuppss  48096  islininds2  48213  zlmodzxzldeplem3  48231  2itscp  48515  reutruALT  48538  alsi-no-surprise  48890