Theorem anbi12i 628

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 623	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜃))
3		anbi12.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	bianbi 627	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  629  an2anr  636  ordi  1007  ordir  1008  orddi  1011  pm5.17  1013  xor  1016  cases2  1047  3anbi123i  1155  an6  1447  nanbi  1500  cadan  1609  nic-axALT  1674  19.43OLD  1883  sbbi  2309  aaan  2333  sbnf2  2361  eubii  2585  cbveuvw  2605  cbveuw  2606  cbveuALT  2608  2mo2  2647  2eu4  2655  sbabel  2932  neanior  3026  r19.26m  3098  reeanlem  3216  2ralorOLD  3220  rexeqbii  3328  reu5  3366  cbvreuw  3394  cgsex4g  3512  reu2  3713  reu3  3715  2reu5a  3732  2reu5lem3  3745  2reu1  3877  eqss  3979  unss  4170  ralunb  4177  ssin  4219  undi  4265  indifdi  4274  undif3  4280  inab  4289  difab  4290  reuss2  4306  reupick  4309  2reu4lem  4502  reuprg  4684  sstp  4817  tpss  4818  prneimg  4835  prneimg2  4836  prnebg  4837  uniin  4912  intun  4961  disjiun  5112  disjxiun  5121  brin  5176  brdif  5177  ssext  5434  pweqb  5436  opthg2  5459  copsex4g  5475  propeqop  5487  eqopab2bw  5528  eqopab2b  5532  pwin  5549  pofun  5584  dffr6  5614  wetrep  5652  elxp3  5725  soinxp  5741  weinxp  5744  csbxp  5759  relun  5795  inopab  5813  difopab  5814  difopabOLD  5815  inxp  5816  inxpOLD  5817  opelco2g  5852  cnvco  5870  dmin  5896  restidsing  6045  intasym  6109  asymref  6110  asymref2  6111  cnvdif  6137  xpnz  6153  difxp  6158  xpdifid  6162  xp11  6169  dfco2  6239  relssdmrnOLD  6263  cnvpo  6281  cnvso  6282  xpco  6283  reu3op  6286  dfpo2  6290  dffun4  6552  funun  6587  fun11  6615  fununi  6616  imadif  6625  fnres  6670  mptfnf  6678  fnopabg  6680  fun  6745  fin  6763  dff1o2  6828  brprcneu  6871  brprcneuALT  6872  dffv2  6979  fsn  7130  f13dfv  7272  dff1o6  7273  isotr  7334  eqoprab2bw  7482  eqoprab2b  7483  fvmpopr2d  7574  porpss  7726  epweon  7774  onsucb  7816  resf1extb  7935  elxp6  8027  dfoprab3  8058  opiota  8063  poxp  8132  soxp  8133  poxp2  8147  xpord2pred  8149  xpord2indlem  8151  xpord3pred  8156  xpord3inddlem  8158  soseq  8163  suppvalbr  8168  brtpos2  8236  frrlem9  8298  fprlem1  8304  wfrlem5OLD  8332  wfrfunOLD  8338  tfrlem7  8402  dfer2  8725  eqer  8760  iiner  8808  uniinqs  8816  brecop  8829  eroveu  8831  erovlem  8832  fsetexb  8883  mapval2  8891  ixpin  8942  boxriin  8959  brsdom  8994  xpcomco  9081  xpassen  9085  sbthlem9  9110  sbthlem10  9111  brsdom2  9116  ssenen  9170  sbthfilem  9217  dffi3  9448  dfsup2  9461  infcllem  9505  axinf2  9659  zfinf2  9661  oemapso  9701  ttrcltr  9735  frrlem15  9776  scottexs  9906  scott0s  9907  kardex  9913  karden  9914  dfac5lem1  10142  dfac5lem3  10144  kmlem15  10184  enfin2i  10340  fin23lem34  10365  brdom7disj  10550  fpwwe2lem11  10660  fpwwe2lem12  10661  axgroth5  10843  grothprim  10853  addsrpr  11094  mulsrpr  11095  mulgt0sr  11124  addcnsr  11154  mulcnsr  11155  ltresr  11159  axcnre  11183  1re  11240  ssxr  11309  infrenegsup  12230  nnwos  12936  zmin  12965  xrnemnf  13138  xrnepnf  13139  xmullem  13285  xmulcom  13287  xmulneg1  13290  xmulf  13293  xrinfmss2  13332  elfzuzb  13540  fzass4  13584  seqof  14082  hashbclem  14475  hashfacen  14477  xpcogend  14998  trclublem  15019  rexanre  15370  caubnd  15382  o1lo1  15558  rpnnen2lem12  16248  lcmcllem  16620  lcmftp  16660  lcmfunsnlem2  16664  isprm3  16707  prmreclem2  16942  4sqlem12  16981  catcone0  17704  isffth2  17936  fucinv  17994  lublecllem  18375  odulub  18422  oduglb  18424  issubmgm  18685  rabsubmgmd  18687  mndpsuppss  18748  issubm  18786  issubmd  18789  0subm  18800  insubm  18801  sursubmefmnd  18879  injsubmefmnd  18880  smndex1mgm  18890  isnsg2  19144  cycsubm  19190  oppgid  19344  symgfixf1  19423  pmtrrn2  19446  lsmdisjr  19670  lsmhash  19691  gsumcom3  19964  dprd0  20019  issrg  20153  dvdsrtr  20333  isirred2  20386  isdomn3  20680  opprdomnb  20682  isdomn4r  20684  lss1d  20925  lspsolvlem  21108  lbsextlem2  21125  cnfldfun  21334  cnfldfunOLD  21347  unocv  21645  iunocv  21646  evlsval  22049  mpomatmul  22389  cpmidpmat  22816  tgval2  22899  fctop  22947  ppttop  22950  epttop  22952  cnnei  23225  2ndcctbss  23398  txuni2  23508  txbas  23510  ptbasin  23520  txdis1cn  23578  xkococnlem  23602  opnfbas  23785  fgcl  23821  fbasrn  23827  filuni  23828  cfinfil  23836  csdfil  23837  fin1aufil  23875  rnelfmlem  23895  fmfnfmlem3  23899  txflf  23949  xmeterval  24376  reconn  24773  iimulcl  24889  isclmp  25053  iscau3  25235  rrxmvallem  25361  minveclem3  25386  pmltpc  25408  ovolfcl  25424  ismbl  25484  dyaddisj  25554  iblre  25752  plyun0  26159  logfaclbnd  27190  lgslem3  27267  lgsdir2lem5  27297  nosupinfsep  27701  nocvxmin  27747  sltrec  27789  madebdaylemlrcut  27867  addsproplem2  27934  addsuniflem  27965  negsproplem2  27992  negsid  28004  mulsproplem5  28080  mulsproplem6  28081  mulsproplem7  28082  mulsproplem8  28083  mulsproplem9  28084  mulsuniflem  28109  precsexlem9  28174  precsexlem10  28175  nnaddscl  28295  nnmulscl  28296  zaddscl  28339  recut  28404  0reno  28405  readdscl  28407  remulscl  28410  tgjustf  28457  ishpg  28743  usgrexmpllem  29244  nb3grpr2  29367  vtxd0nedgb  29473  wlk1walk  29624  clwlkcompbp  29769  wwlknllvtx  29833  wwlksonvtx  29842  wspthnonp  29846  wwlksn0s  29848  wwlksnndef  29892  2wlkdlem8  29920  elwwlks2s3  29938  clwwlkf1  30035  clwwlknonccat  30082  clwwlknon2x  30089  3pthdlem1  30150  upgr4cycl4dv4e  30171  frgr2wwlk1  30315  frgrreg  30380  ajfval  30795  issh  31194  chcon2i  31450  chcon3i  31452  spanuni  31530  5oalem7  31646  3oalem3  31650  pjin2i  32179  pjin3i  32180  cvnbtwn4  32275  mdslj1i  32305  mdslj2i  32306  mdslmd1i  32315  chrelat4i  32359  chirredi  32380  cdj3i  32427  rmoun  32480  difrab2  32484  eqdif  32505  inpr0  32518  iuninc  32546  fcoinvbr  32591  suppss2f  32621  fmptdF  32639  disjdsct  32685  f1od2  32703  hashxpe  32791  tosglblem  32959  mgcval  32972  pmtrprfv2  33104  elrgspnlem2  33243  ssdifidllem  33476  ssmxidllem  33493  ccfldextdgrr  33718  fldext2chn  33767  ordtconnlem1  33960  esumpfinvalf  34112  esum2dlem  34128  measiuns  34253  eulerpartlemt0  34406  eulerpartlemr  34411  eulerpartlemn  34418  ballotlem2  34526  ballotlemodife  34535  bnj887  34801  bnj976  34813  bnj1385  34868  bnj153  34916  bnj543  34929  bnj607  34952  bnj882  34962  bnj916  34969  bnj983  34987  derangenlem  35198  pconnconn  35258  fmlaomn0  35417  fmla0disjsuc  35425  fmlasucdisj  35426  elmpst  35563  xpab  35748  dftr6  35773  dffr5  35776  fundmpss  35789  elpotr  35804  brtxp  35903  brpprod  35908  brsset  35912  idsset  35913  dfon3  35915  ellimits  35933  dffun10  35937  elfuns  35938  brcart  35955  brimg  35960  brapply  35961  brcap  35963  brsuccf  35964  funpartfun  35966  dfrecs2  35973  dfrdg4  35974  altopthc  35994  altopthd  35995  altopelaltxp  35999  outsideoftr  36152  rmoeqbii  36211  reueqbii  36213  rabeqbii  36217  riotaeqbii  36221  ixpeq1i  36223  cbvixpvw2  36268  cbvprodvw2  36270  trer  36339  neibastop1  36382  neifg  36394  df3nandALT1  36422  imnand2  36425  eliminable-abelab  36893  bj-eldiag2  37200  bj-imdiridlem  37208  bj-opabco  37211  bj-xpcossxp  37212  topdifinfeq  37373  relowlssretop  37386  relowlpssretop  37387  wl-cases2-dnf  37535  poimirlem30  37679  poimirlem32  37681  ismblfin  37690  mbfposadd  37696  inixp  37757  elghomOLD  37916  keridl  38061  smprngopr  38081  sbcani  38137  inxpxrn  38418  dfcoss2  38436  cosscnv  38439  coss1cnvres  38440  coss2cnvepres  38441  1cossres  38452  dfcoels  38453  trressn  38468  br1cossinres  38470  br1cossinidres  38472  br1cossincnvepres  38473  br1cossxrnidres  38474  br1cossxrncnvepres  38475  cosscnvssid3  38499  coss0  38502  cossid  38503  trcoss  38505  eleccossin  38506  dfssr2  38522  br1cossxrncnvssrres  38531  refsymrels3  38589  refsymrel2  38590  refsymrel3  38591  elrefsymrels3  38593  dfeqvrel2  38613  dfeqvrel3  38614  redundeq1  38652  redundpbi1  38654  dfcomember3  38697  eqvreldmqs  38698  eqvreldmqs2  38699  dfeldisj3  38742  eldisjn0elb  38768  antisymrelres  38786  dfmembpart2  38793  prtlem10  38888  prter1  38902  lcvbr3  39046  isopos  39203  llnexatN  39545  snatpsubN  39774  pclclN  39915  pclfinN  39924  lhpocnel2  40043  cdlemk19w  40996  dih1dimatlem  41353  psspwb  42246  redvmptabs  42378  mzpclall  42725  mzpincl  42732  mzpindd  42744  2nn0ind  42944  dford4  43028  wopprc  43029  islmodfg  43068  ifpan123g  43458  ifpan23  43459  ifpnot23  43477  ifpdfxor  43486  ifpidg  43490  ifpid1g  43493  ifpim23g  43494  ifpim123g  43499  ifpim1g  43500  ifp1bi  43501  ifpimimb  43503  ifpororb  43504  ifpor123g  43507  ifpbibib  43509  rp-isfinite6  43517  alephiso2  43557  undmrnresiss  43603  cotrintab  43613  brtrclfv2  43726  dfxor4  43765  snhesn  43785  dffrege76  43938  uneqsn  44024  expandan  44287  ismnuprim  44293  nzin  44317  onfrALTlem5  44542  onfrALTlem4  44543  undif3VD  44881  onfrALTlem5VD  44884  onfrALTlem4VD  44885  dfac5prim  44990  wfaxpr  44998  brpermmodel  45003  permac8prim  45014  ndisj2  45055  rexabsle  45426  ellimcabssub0  45626  limsupre2mpt  45739  limsupre3  45742  limsupre3mpt  45743  limsupre3uz  45745  limsupreuz  45746  liminfreuz  45812  fourierdlem103  46218  fourierdlem104  46219  fourierdlem112  46227  smflim  46786  smflim2  46815  smflimsuplem1  46829  smflimsup  46837  cfsetsnfsetf1  47068  2reu8i  47122  ichan  47449  clnbgrsym  47831  dfnbgr6  47850  upgrimpthslem2  47901  isgrlim  47974  usgrexmpl2trifr  48021  2zlidl  48195  islininds2  48440  zlmodzxzldeplem3  48458  2itscp  48741  reutruALT  48764  iinxp  48789  0funclem  49031  fucofulem2  49202  fuco2el  49203  2arwcatlem1  49452  alsi-no-surprise  49640