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  2307  aaan  2331  sbnf2  2356  eubii  2578  cbveuvw  2598  cbveuw  2599  cbveuALT  2601  2mo2  2640  2eu4  2648  sbabel  2924  neanior  3018  r19.26m  3090  reeanlem  3208  rexeqbii  3318  reu5  3356  cbvreuw  3382  cgsex4g  3494  reu2  3696  reu3  3698  2reu5a  3715  2reu5lem3  3728  2reu1  3860  eqss  3962  unss  4153  ralunb  4160  ssin  4202  undi  4248  indifdi  4257  undif3  4263  inab  4272  difab  4273  reuss2  4289  reupick  4292  2reu4lem  4485  reuprg  4667  sstp  4800  tpss  4801  prneimg  4818  prneimg2  4819  prnebg  4820  uniin  4895  intun  4944  disjiun  5095  disjxiun  5104  brin  5159  brdif  5160  ssext  5414  pweqb  5416  opthg2  5439  copsex4g  5455  propeqop  5467  eqopab2bw  5508  eqopab2b  5512  pwin  5529  pofun  5564  dffr6  5594  wetrep  5631  elxp3  5704  soinxp  5720  weinxp  5723  csbxp  5738  relun  5774  inopab  5792  difopab  5793  difopabOLD  5794  inxp  5795  inxpOLD  5796  opelco2g  5831  cnvco  5849  dmin  5875  restidsing  6024  intasym  6088  asymref  6089  asymref2  6090  cnvdif  6116  xpnz  6132  difxp  6137  xpdifid  6141  xp11  6148  dfco2  6218  relssdmrnOLD  6242  cnvpo  6260  cnvso  6261  xpco  6262  reu3op  6265  dfpo2  6269  dffun4  6527  funun  6562  fun11  6590  fununi  6591  imadif  6600  fnres  6645  mptfnf  6653  fnopabg  6655  fun  6722  fin  6740  dff1o2  6805  brprcneu  6848  brprcneuALT  6849  dffv2  6956  fsn  7107  f13dfv  7249  dff1o6  7250  isotr  7311  eqoprab2bw  7459  eqoprab2b  7460  fvmpopr2d  7551  porpss  7703  epweon  7751  onsucb  7792  resf1extb  7910  elxp6  8002  dfoprab3  8033  opiota  8038  poxp  8107  soxp  8108  poxp2  8122  xpord2pred  8124  xpord2indlem  8126  xpord3pred  8131  xpord3inddlem  8133  soseq  8138  suppvalbr  8143  brtpos2  8211  frrlem9  8273  fprlem1  8279  tfrlem7  8351  dfer2  8672  eqer  8707  iiner  8762  uniinqs  8770  brecop  8783  eroveu  8785  erovlem  8786  fsetexb  8837  mapval2  8845  ixpin  8896  boxriin  8913  brsdom  8946  xpcomco  9031  xpassen  9035  sbthlem9  9059  sbthlem10  9060  brsdom2  9065  ssenen  9115  sbthfilem  9162  dffi3  9382  dfsup2  9395  infcllem  9439  axinf2  9593  zfinf2  9595  oemapso  9635  ttrcltr  9669  frrlem15  9710  scottexs  9840  scott0s  9841  kardex  9847  karden  9848  dfac5lem1  10076  dfac5lem3  10078  kmlem15  10118  enfin2i  10274  fin23lem34  10299  brdom7disj  10484  fpwwe2lem11  10594  fpwwe2lem12  10595  axgroth5  10777  grothprim  10787  addsrpr  11028  mulsrpr  11029  mulgt0sr  11058  addcnsr  11088  mulcnsr  11089  ltresr  11093  axcnre  11117  ssxr  11243  infrenegsup  12166  nnwos  12874  zmin  12903  xrnemnf  13077  xrnepnf  13078  xmullem  13224  xmulcom  13226  xmulneg1  13229  xmulf  13232  xrinfmss2  13271  elfzuzb  13479  fzass4  13523  seqof  14024  hashbclem  14417  hashfacen  14419  xpcogend  14940  trclublem  14961  rexanre  15313  caubnd  15325  o1lo1  15503  rpnnen2lem12  16193  lcmcllem  16566  lcmftp  16606  lcmfunsnlem2  16610  isprm3  16653  prmreclem2  16888  4sqlem12  16927  catcone0  17648  isffth2  17880  fucinv  17938  lublecllem  18319  odulub  18366  oduglb  18368  issubmgm  18629  rabsubmgmd  18631  mndpsuppss  18692  issubm  18730  issubmd  18733  0subm  18744  insubm  18745  sursubmefmnd  18823  injsubmefmnd  18824  smndex1mgm  18834  isnsg2  19088  cycsubm  19134  oppgid  19288  symgfixf1  19367  pmtrrn2  19390  lsmdisjr  19614  lsmhash  19635  gsumcom3  19908  dprd0  19963  issrg  20097  dvdsrtr  20277  isirred2  20330  isdomn3  20624  opprdomnb  20626  isdomn4r  20628  lss1d  20869  lspsolvlem  21052  lbsextlem2  21069  cnfldfun  21278  cnfldfunOLD  21291  unocv  21589  iunocv  21590  evlsval  21993  mpomatmul  22333  cpmidpmat  22760  tgval2  22843  fctop  22891  ppttop  22894  epttop  22896  cnnei  23169  2ndcctbss  23342  txuni2  23452  txbas  23454  ptbasin  23464  txdis1cn  23522  xkococnlem  23546  opnfbas  23729  fgcl  23765  fbasrn  23771  filuni  23772  cfinfil  23780  csdfil  23781  fin1aufil  23819  rnelfmlem  23839  fmfnfmlem3  23843  txflf  23893  xmeterval  24320  reconn  24717  iimulcl  24833  isclmp  24997  iscau3  25178  rrxmvallem  25304  minveclem3  25329  pmltpc  25351  ovolfcl  25367  ismbl  25427  dyaddisj  25497  iblre  25695  plyun0  26102  logfaclbnd  27133  lgslem3  27210  lgsdir2lem5  27240  nosupinfsep  27644  nocvxmin  27690  sltrec  27732  madebdaylemlrcut  27810  addsproplem2  27877  addsuniflem  27908  negsproplem2  27935  negsid  27947  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  mulsproplem9  28027  mulsuniflem  28052  precsexlem9  28117  precsexlem10  28118  nnaddscl  28238  nnmulscl  28239  zaddscl  28282  recut  28347  0reno  28348  readdscl  28350  remulscl  28353  tgjustf  28400  ishpg  28686  usgrexmpllem  29187  nb3grpr2  29310  vtxd0nedgb  29416  wlk1walk  29567  clwlkcompbp  29712  wwlknllvtx  29776  wwlksonvtx  29785  wspthnonp  29789  wwlksn0s  29791  wwlksnndef  29835  2wlkdlem8  29863  elwwlks2s3  29881  clwwlkf1  29978  clwwlknonccat  30025  clwwlknon2x  30032  3pthdlem1  30093  upgr4cycl4dv4e  30114  frgr2wwlk1  30258  frgrreg  30323  ajfval  30738  issh  31137  chcon2i  31393  chcon3i  31395  spanuni  31473  5oalem7  31589  3oalem3  31593  pjin2i  32122  pjin3i  32123  cvnbtwn4  32218  mdslj1i  32248  mdslj2i  32249  mdslmd1i  32258  chrelat4i  32302  chirredi  32323  cdj3i  32370  rmoun  32423  difrab2  32427  eqdif  32448  inpr0  32461  iuninc  32489  fcoinvbr  32534  suppss2f  32562  fmptdF  32580  disjdsct  32626  f1od2  32644  hashxpe  32732  tosglblem  32900  mgcval  32913  pmtrprfv2  33045  elrgspnlem2  33194  ssdifidllem  33427  ssmxidllem  33444  ccfldextdgrr  33667  fldext2chn  33718  ordtconnlem1  33914  esumpfinvalf  34066  esum2dlem  34082  measiuns  34207  eulerpartlemt0  34360  eulerpartlemr  34365  eulerpartlemn  34372  ballotlem2  34480  ballotlemodife  34489  bnj887  34755  bnj976  34767  bnj1385  34822  bnj153  34870  bnj543  34883  bnj607  34906  bnj882  34916  bnj916  34923  bnj983  34941  derangenlem  35158  pconnconn  35218  fmlaomn0  35377  fmla0disjsuc  35385  fmlasucdisj  35386  elmpst  35523  xpab  35713  dftr6  35738  dffr5  35741  fundmpss  35754  elpotr  35769  brtxp  35868  brpprod  35873  brsset  35877  idsset  35878  dfon3  35880  ellimits  35898  dffun10  35902  elfuns  35903  brcart  35920  brimg  35925  brapply  35926  brcap  35928  brsuccf  35929  funpartfun  35931  dfrecs2  35938  dfrdg4  35939  altopthc  35959  altopthd  35960  altopelaltxp  35964  outsideoftr  36117  rmoeqbii  36176  reueqbii  36178  rabeqbii  36182  riotaeqbii  36186  ixpeq1i  36188  cbvixpvw2  36233  cbvprodvw2  36235  trer  36304  neibastop1  36347  neifg  36359  df3nandALT1  36387  imnand2  36390  eliminable-abelab  36858  bj-eldiag2  37165  bj-imdiridlem  37173  bj-opabco  37176  bj-xpcossxp  37177  topdifinfeq  37338  relowlssretop  37351  relowlpssretop  37352  wl-cases2-dnf  37500  poimirlem30  37644  poimirlem32  37646  ismblfin  37655  mbfposadd  37661  inixp  37722  elghomOLD  37881  keridl  38026  smprngopr  38046  sbcani  38102  inxpxrn  38381  dfcoss2  38404  cosscnv  38407  coss1cnvres  38408  coss2cnvepres  38409  1cossres  38420  dfcoels  38421  trressn  38436  br1cossinres  38438  br1cossinidres  38440  br1cossincnvepres  38441  br1cossxrnidres  38442  br1cossxrncnvepres  38443  cosscnvssid3  38467  coss0  38470  cossid  38471  trcoss  38473  eleccossin  38474  dfssr2  38490  br1cossxrncnvssrres  38499  refsymrels3  38557  refsymrel2  38558  refsymrel3  38559  elrefsymrels3  38561  dfeqvrel2  38581  dfeqvrel3  38582  redundeq1  38620  redundpbi1  38622  dfcomember3  38666  eqvreldmqs  38667  eqvreldmqs2  38668  dfeldisj3  38711  eldisjn0elb  38737  antisymrelres  38755  dfmembpart2  38762  prtlem10  38858  prter1  38872  lcvbr3  39016  isopos  39173  llnexatN  39515  snatpsubN  39744  pclclN  39885  pclfinN  39894  lhpocnel2  40013  cdlemk19w  40966  dih1dimatlem  41323  psspwb  42216  redvmptabs  42348  mzpclall  42715  mzpincl  42722  mzpindd  42734  2nn0ind  42934  dford4  43018  wopprc  43019  islmodfg  43058  ifpan123g  43448  ifpan23  43449  ifpnot23  43467  ifpdfxor  43476  ifpidg  43480  ifpid1g  43483  ifpim23g  43484  ifpim123g  43489  ifpim1g  43490  ifp1bi  43491  ifpimimb  43493  ifpororb  43494  ifpor123g  43497  ifpbibib  43499  rp-isfinite6  43507  alephiso2  43547  undmrnresiss  43593  cotrintab  43603  brtrclfv2  43716  dfxor4  43755  snhesn  43775  dffrege76  43928  uneqsn  44014  expandan  44277  ismnuprim  44283  nzin  44307  onfrALTlem5  44532  onfrALTlem4  44533  undif3VD  44871  onfrALTlem5VD  44874  onfrALTlem4VD  44875  dfac5prim  44980  wfaxpr  44988  brpermmodel  44993  permac8prim  45004  ndisj2  45045  rexabsle  45415  ellimcabssub0  45615  limsupre2mpt  45728  limsupre3  45731  limsupre3mpt  45732  limsupre3uz  45734  limsupreuz  45735  liminfreuz  45801  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  smflim  46775  smflim2  46804  smflimsuplem1  46818  smflimsup  46826  cfsetsnfsetf1  47060  2reu8i  47114  ichan  47456  clnbgrsym  47838  dfnbgr6  47857  upgrimpthslem2  47908  isgrlim  47981  usgrexmpl2trifr  48028  pgnbgreunbgrlem5  48113  pgnbgreunbgr  48115  2zlidl  48228  islininds2  48473  zlmodzxzldeplem3  48491  2itscp  48770  reutruALT  48793  iinxp  48819  0funclem  49075  fucofulem2  49300  fuco2el  49301  catcinv  49388  2arwcatlem1  49584  alsi-no-surprise  49785