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  3317  reu5  3354  cbvreuw  3378  cgsex4g  3489  reu2  3685  reu3  3687  2reu5a  3704  2reu5lem3  3717  2reu1  3849  eqss  3951  unss  4144  ralunb  4151  ssin  4193  undi  4239  indifdi  4248  undif3  4254  inab  4263  difab  4264  reuss2  4280  reupick  4283  2reu4lem  4478  reuprg  4662  sstp  4794  tpss  4795  prneimg  4812  prneimg2  4813  prnebg  4814  uniin  4889  intun  4937  disjiun  5088  disjxiun  5097  brin  5152  brdif  5153  ssext  5409  pweqb  5411  opthg2  5435  copsex4g  5451  propeqop  5463  eqopab2bw  5504  eqopab2b  5508  pwin  5523  pofun  5558  dffr6  5588  wetrep  5625  elxp3  5698  soinxp  5714  weinxp  5717  csbxp  5733  relun  5768  inopab  5786  difopab  5787  inxp  5788  inxpOLD  5789  opelco2g  5824  cnvco  5842  dmin  5868  restidsing  6020  intasym  6080  asymref  6081  asymref2  6082  cnvdif  6109  xpnz  6125  difxp  6130  xpdifid  6134  xp11  6141  dfco2  6211  cnvpo  6253  cnvso  6254  xpco  6255  reu3op  6258  dfpo2  6262  dffun4  6513  funun  6546  fun11  6574  fununi  6575  imadif  6584  fnres  6627  mptfnf  6635  fnopabg  6637  fun  6704  fin  6722  dff1o2  6787  brprcneu  6832  brprcneuALT  6833  dffv2  6937  fsn  7090  f13dfv  7230  dff1o6  7231  isotr  7292  eqoprab2bw  7438  eqoprab2b  7439  fvmpopr2d  7530  porpss  7682  epweon  7730  onsucb  7769  resf1extb  7886  elxp6  7977  dfoprab3  8008  opiota  8013  poxp  8080  soxp  8081  poxp2  8095  xpord2pred  8097  xpord2indlem  8099  xpord3pred  8104  xpord3inddlem  8106  soseq  8111  suppvalbr  8116  brtpos2  8184  frrlem9  8246  fprlem1  8252  tfrlem7  8324  dfer2  8646  eqer  8682  iiner  8738  uniinqs  8746  brecop  8759  eroveu  8761  erovlem  8762  fsetexb  8813  mapval2  8822  ixpin  8873  boxriin  8890  brsdom  8923  xpcomco  9007  xpassen  9011  sbthlem9  9035  sbthlem10  9036  brsdom2  9041  ssenen  9091  sbthfilem  9134  dffi3  9346  dfsup2  9359  infcllem  9403  axinf2  9561  zfinf2  9563  oemapso  9603  ttrcltr  9637  frrlem15  9681  scottexs  9811  scott0s  9812  kardex  9818  karden  9819  dfac5lem1  10045  dfac5lem3  10047  kmlem15  10087  enfin2i  10243  fin23lem34  10268  brdom7disj  10453  fpwwe2lem11  10564  fpwwe2lem12  10565  axgroth5  10747  grothprim  10757  addsrpr  10998  mulsrpr  10999  mulgt0sr  11028  addcnsr  11058  mulcnsr  11059  ltresr  11063  axcnre  11087  ssxr  11214  infrenegsup  12137  nnwos  12840  zmin  12869  xrnemnf  13043  xrnepnf  13044  xmullem  13191  xmulcom  13193  xmulneg1  13196  xmulf  13199  xrinfmss2  13238  elfzuzb  13446  fzass4  13490  seqof  13994  hashbclem  14387  hashfacen  14389  xpcogend  14909  trclublem  14930  rexanre  15282  caubnd  15294  o1lo1  15472  rpnnen2lem12  16162  lcmcllem  16535  lcmftp  16575  lcmfunsnlem2  16579  isprm3  16622  prmreclem2  16857  4sqlem12  16896  catcone0  17622  isffth2  17854  fucinv  17912  lublecllem  18293  odulub  18340  oduglb  18342  issubmgm  18639  rabsubmgmd  18641  mndpsuppss  18702  issubm  18740  issubmd  18743  0subm  18754  insubm  18755  sursubmefmnd  18833  injsubmefmnd  18834  smndex1mgm  18844  isnsg2  19097  cycsubm  19143  oppgid  19297  symgfixf1  19378  pmtrrn2  19401  lsmdisjr  19625  lsmhash  19646  gsumcom3  19919  dprd0  19974  issrg  20135  dvdsrtr  20316  isirred2  20369  isdomn3  20660  opprdomnb  20662  isdomn4r  20664  lss1d  20926  lspsolvlem  21109  lbsextlem2  21126  cnfldfun  21335  cnfldfunOLD  21348  unocv  21647  iunocv  21648  evlsval  22053  mpomatmul  22402  cpmidpmat  22829  tgval2  22912  fctop  22960  ppttop  22963  epttop  22965  cnnei  23238  2ndcctbss  23411  txuni2  23521  txbas  23523  ptbasin  23533  txdis1cn  23591  xkococnlem  23615  opnfbas  23798  fgcl  23834  fbasrn  23840  filuni  23841  cfinfil  23849  csdfil  23850  fin1aufil  23888  rnelfmlem  23908  fmfnfmlem3  23912  txflf  23962  xmeterval  24388  reconn  24785  iimulcl  24901  isclmp  25065  iscau3  25246  rrxmvallem  25372  minveclem3  25397  pmltpc  25419  ovolfcl  25435  ismbl  25495  dyaddisj  25565  iblre  25763  plyun0  26170  logfaclbnd  27201  lgslem3  27278  lgsdir2lem5  27308  nosupinfsep  27712  ltsrec  27809  madebdaylemlrcut  27907  addsproplem2  27978  addsuniflem  28009  negsproplem2  28037  negsid  28049  mulsproplem5  28128  mulsproplem6  28129  mulsproplem7  28130  mulsproplem8  28131  mulsproplem9  28132  mulsuniflem  28157  precsexlem9  28223  precsexlem10  28224  ons2ind  28283  nnaddscl  28354  nnmulscl  28355  zaddscl  28402  zsoring  28417  recut  28502  readdscl  28507  remulscl  28510  tgjustf  28557  ishpg  28843  usgrexmpllem  29345  nb3grpr2  29468  vtxd0nedgb  29574  wlk1walk  29724  clwlkcompbp  29867  wwlknllvtx  29931  wwlksonvtx  29940  wspthnonp  29944  wwlksn0s  29946  wwlksnndef  29990  2wlkdlem8  30018  elwwlks2s3  30036  clwwlkf1  30136  clwwlknonccat  30183  clwwlknon2x  30190  3pthdlem1  30251  upgr4cycl4dv4e  30272  frgr2wwlk1  30416  frgrreg  30481  ajfval  30897  issh  31296  chcon2i  31552  chcon3i  31554  spanuni  31632  5oalem7  31748  3oalem3  31752  pjin2i  32281  pjin3i  32282  cvnbtwn4  32377  mdslj1i  32407  mdslj2i  32408  mdslmd1i  32417  chrelat4i  32461  chirredi  32482  cdj3i  32529  rmoun  32580  difrab2  32584  eqdif  32606  inpr0  32619  iuninc  32647  fcoinvbr  32692  suppss2f  32728  fmptdF  32746  disjdsct  32793  f1od2  32809  hashxpe  32898  tosglblem  33067  mgcval  33080  pmtrprfv2  33182  elrgspnlem2  33337  ssdifidllem  33549  ssmxidllem  33566  ccfldextdgrr  33850  fldext2chn  33906  ordtconnlem1  34102  esumpfinvalf  34254  esum2dlem  34270  measiuns  34395  eulerpartlemt0  34547  eulerpartlemr  34552  eulerpartlemn  34559  ballotlem2  34667  ballotlemodife  34676  bnj887  34942  bnj976  34954  bnj1385  35008  bnj153  35056  bnj543  35069  bnj607  35092  bnj882  35102  bnj916  35109  bnj983  35127  axreg  35305  axregscl  35306  axregs  35317  derangenlem  35387  pconnconn  35447  fmlaomn0  35606  fmla0disjsuc  35614  fmlasucdisj  35615  elmpst  35752  xpab  35942  dftr6  35967  dffr5  35970  fundmpss  35983  elpotr  35995  brtxp  36094  brpprod  36099  brsset  36103  idsset  36104  dfon3  36106  ellimits  36124  dffun10  36128  elfuns  36129  brcart  36146  brimg  36151  brapply  36152  brcap  36154  lemsuccf  36155  funpartfun  36159  dfrecs2  36166  dfrdg4  36167  altopthc  36187  altopthd  36188  altopelaltxp  36192  outsideoftr  36345  rmoeqbii  36404  reueqbii  36406  rabeqbii  36410  riotaeqbii  36414  ixpeq1i  36416  cbvixpvw2  36461  cbvprodvw2  36463  trer  36532  neibastop1  36575  neifg  36587  df3nandALT1  36615  imnand2  36618  regsfromregtr  36690  regsfromunir1  36692  eliminable-abelab  37118  bj-eldiag2  37432  bj-imdiridlem  37440  bj-opabco  37443  bj-xpcossxp  37444  topdifinfeq  37605  relowlssretop  37618  relowlpssretop  37619  wl-cases2-dnf  37767  poimirlem30  37901  poimirlem32  37903  ismblfin  37912  mbfposadd  37918  inixp  37979  elghomOLD  38138  keridl  38283  smprngopr  38303  sbcani  38359  inxpxrn  38669  dfcoss2  38754  cosscnv  38757  coss1cnvres  38758  coss2cnvepres  38759  1cossres  38770  dfcoels  38771  trressn  38786  br1cossinres  38788  br1cossinidres  38790  br1cossincnvepres  38791  br1cossxrnidres  38792  br1cossxrncnvepres  38793  cosscnvssid3  38817  coss0  38820  cossid  38821  trcoss  38823  eleccossin  38824  dfssr2  38830  br1cossxrncnvssrres  38839  refsymrels3  38901  refsymrel2  38902  refsymrel3  38903  elrefsymrels3  38905  dfeqvrel2  38925  dfeqvrel3  38926  redundeq1  38964  redundpbi1  38966  dfcomember3  39010  eqvreldmqs  39011  eqvreldmqs2  39012  dfeldisj3  39062  eldisjdmqsim  39068  eldisjn0elb  39096  antisymrelres  39117  dfmembpart2  39124  prtlem10  39241  prter1  39255  lcvbr3  39399  isopos  39556  llnexatN  39897  snatpsubN  40126  pclclN  40267  pclfinN  40276  lhpocnel2  40395  cdlemk19w  41348  dih1dimatlem  41705  psspwb  42600  redvmptabs  42730  mzpclall  43084  mzpincl  43091  mzpindd  43103  2nn0ind  43302  dford4  43386  wopprc  43387  islmodfg  43426  ifpan123g  43815  ifpan23  43816  ifpnot23  43834  ifpdfxor  43843  ifpidg  43847  ifpid1g  43850  ifpim23g  43851  ifpim123g  43856  ifpim1g  43857  ifp1bi  43858  ifpimimb  43860  ifpororb  43861  ifpor123g  43864  ifpbibib  43866  rp-isfinite6  43874  alephiso2  43914  undmrnresiss  43960  cotrintab  43970  brtrclfv2  44083  dfxor4  44122  snhesn  44142  dffrege76  44295  uneqsn  44381  expandan  44644  ismnuprim  44650  nzin  44674  onfrALTlem5  44898  onfrALTlem4  44899  undif3VD  45237  onfrALTlem5VD  45240  onfrALTlem4VD  45241  dfac5prim  45346  wfaxpr  45354  brpermmodel  45359  permac8prim  45370  ndisj2  45411  rexabsle  45777  ellimcabssub0  45977  limsupre2mpt  46088  limsupre3  46091  limsupre3mpt  46092  limsupre3uz  46094  limsupreuz  46095  liminfreuz  46161  fourierdlem103  46567  fourierdlem104  46568  fourierdlem112  46576  smflim  47135  smflim2  47164  smflimsuplem1  47178  smflimsup  47186  cfsetsnfsetf1  47419  2reu8i  47473  ichan  47815  clnbgrsym  48198  dfnbgr6  48217  upgrimpthslem2  48268  isgrlim  48342  usgrexmpl2trifr  48397  pgnbgreunbgrlem5  48483  pgnbgreunbgr  48485  2zlidl  48600  islininds2  48844  zlmodzxzldeplem3  48862  2itscp  49141  reutruALT  49164  iinxp  49190  0funclem  49445  fucofulem2  49670  fuco2el  49671  catcinv  49758  2arwcatlem1  49954  alsi-no-surprise  50155