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  3311  reu5  3345  cbvreuw  3369  cgsex4g  3477  reu2  3672  reu3  3674  2reu5a  3691  2reu5lem3  3704  2reu1  3836  eqss  3938  unss  4131  ralunb  4138  ssin  4180  undi  4226  indifdi  4235  undif3  4241  inab  4250  difab  4251  reuss2  4267  reupick  4270  2reu4lem  4464  reuprg  4648  sstp  4780  tpss  4781  prneimg  4798  prneimg2  4799  prnebg  4800  uniin  4875  intun  4923  disjiun  5074  disjxiun  5083  brin  5138  brdif  5139  ssext  5399  pweqb  5401  opthg2  5425  copsex4g  5441  propeqop  5453  eqopab2bw  5494  eqopab2b  5498  pwin  5513  pofun  5548  dffr6  5578  wetrep  5615  elxp3  5688  soinxp  5704  weinxp  5707  csbxp  5723  relun  5758  inopab  5776  difopab  5777  inxp  5778  inxpOLD  5779  opelco2g  5814  cnvco  5832  dmin  5858  restidsing  6010  intasym  6070  asymref  6071  asymref2  6072  cnvdif  6099  xpnz  6115  difxp  6120  xpdifid  6124  xp11  6131  dfco2  6201  cnvpo  6243  cnvso  6244  xpco  6245  reu3op  6248  dfpo2  6252  dffun4  6503  funun  6536  fun11  6564  fununi  6565  imadif  6574  fnres  6617  mptfnf  6625  fnopabg  6627  fun  6694  fin  6712  dff1o2  6777  brprcneu  6822  brprcneuALT  6823  dffv2  6927  fsn  7080  f13dfv  7220  dff1o6  7221  isotr  7282  eqoprab2bw  7428  eqoprab2b  7429  fvmpopr2d  7520  porpss  7672  epweon  7720  onsucb  7759  resf1extb  7876  elxp6  7967  dfoprab3  7998  opiota  8003  poxp  8069  soxp  8070  poxp2  8084  xpord2pred  8086  xpord2indlem  8088  xpord3pred  8093  xpord3inddlem  8095  soseq  8100  suppvalbr  8105  brtpos2  8173  frrlem9  8235  fprlem1  8241  tfrlem7  8313  dfer2  8635  eqer  8671  iiner  8727  uniinqs  8735  brecop  8748  eroveu  8750  erovlem  8751  fsetexb  8802  mapval2  8811  ixpin  8862  boxriin  8879  brsdom  8912  xpcomco  8996  xpassen  9000  sbthlem9  9024  sbthlem10  9025  brsdom2  9030  ssenen  9080  sbthfilem  9123  dffi3  9335  dfsup2  9348  infcllem  9392  axinf2  9550  zfinf2  9552  oemapso  9592  ttrcltr  9626  frrlem15  9670  scottexs  9800  scott0s  9801  kardex  9807  karden  9808  dfac5lem1  10034  dfac5lem3  10036  kmlem15  10076  enfin2i  10232  fin23lem34  10257  brdom7disj  10442  fpwwe2lem11  10553  fpwwe2lem12  10554  axgroth5  10736  grothprim  10746  addsrpr  10987  mulsrpr  10988  mulgt0sr  11017  addcnsr  11047  mulcnsr  11048  ltresr  11052  axcnre  11076  ssxr  11204  infrenegsup  12128  nnwos  12854  zmin  12883  xrnemnf  13057  xrnepnf  13058  xmullem  13205  xmulcom  13207  xmulneg1  13210  xmulf  13213  xrinfmss2  13252  elfzuzb  13461  fzass4  13505  seqof  14010  hashbclem  14403  hashfacen  14405  xpcogend  14925  trclublem  14946  rexanre  15298  caubnd  15310  o1lo1  15488  rpnnen2lem12  16181  lcmcllem  16554  lcmftp  16594  lcmfunsnlem2  16598  isprm3  16641  prmreclem2  16877  4sqlem12  16916  catcone0  17642  isffth2  17874  fucinv  17932  lublecllem  18313  odulub  18360  oduglb  18362  issubmgm  18659  rabsubmgmd  18661  mndpsuppss  18722  issubm  18760  issubmd  18763  0subm  18774  insubm  18775  sursubmefmnd  18853  injsubmefmnd  18854  smndex1mgm  18867  isnsg2  19120  cycsubm  19166  oppgid  19320  symgfixf1  19401  pmtrrn2  19424  lsmdisjr  19648  lsmhash  19669  gsumcom3  19942  dprd0  19997  issrg  20158  dvdsrtr  20337  isirred2  20390  isdomn3  20681  opprdomnb  20683  isdomn4r  20685  lss1d  20947  lspsolvlem  21130  lbsextlem2  21147  cnfldfun  21356  cnfldfunOLD  21369  unocv  21668  iunocv  21669  evlsval  22073  mpomatmul  22420  cpmidpmat  22847  tgval2  22930  fctop  22978  ppttop  22981  epttop  22983  cnnei  23256  2ndcctbss  23429  txuni2  23539  txbas  23541  ptbasin  23551  txdis1cn  23609  xkococnlem  23633  opnfbas  23816  fgcl  23852  fbasrn  23858  filuni  23859  cfinfil  23867  csdfil  23868  fin1aufil  23906  rnelfmlem  23926  fmfnfmlem3  23930  txflf  23980  xmeterval  24406  reconn  24803  iimulcl  24913  isclmp  25073  iscau3  25254  rrxmvallem  25380  minveclem3  25405  pmltpc  25426  ovolfcl  25442  ismbl  25502  dyaddisj  25572  iblre  25770  plyun0  26174  logfaclbnd  27204  lgslem3  27281  lgsdir2lem5  27311  nosupinfsep  27715  ltsrec  27812  madebdaylemlrcut  27910  addsproplem2  27981  addsuniflem  28012  negsproplem2  28040  negsid  28052  mulsproplem5  28131  mulsproplem6  28132  mulsproplem7  28133  mulsproplem8  28134  mulsproplem9  28135  mulsuniflem  28160  precsexlem9  28226  precsexlem10  28227  ons2ind  28286  nnaddscl  28357  nnmulscl  28358  zaddscl  28405  zsoring  28420  recut  28505  readdscl  28510  remulscl  28513  tgjustf  28560  ishpg  28846  usgrexmpllem  29348  nb3grpr2  29471  vtxd0nedgb  29577  wlk1walk  29727  clwlkcompbp  29870  wwlknllvtx  29934  wwlksonvtx  29943  wspthnonp  29947  wwlksn0s  29949  wwlksnndef  29993  2wlkdlem8  30021  elwwlks2s3  30039  clwwlkf1  30139  clwwlknonccat  30186  clwwlknon2x  30193  3pthdlem1  30254  upgr4cycl4dv4e  30275  frgr2wwlk1  30419  frgrreg  30484  ajfval  30900  issh  31299  chcon2i  31555  chcon3i  31557  spanuni  31635  5oalem7  31751  3oalem3  31755  pjin2i  32284  pjin3i  32285  cvnbtwn4  32380  mdslj1i  32410  mdslj2i  32411  mdslmd1i  32420  chrelat4i  32464  chirredi  32485  cdj3i  32532  rmoun  32583  difrab2  32587  eqdif  32609  inpr0  32622  iuninc  32650  fcoinvbr  32695  suppss2f  32731  fmptdF  32749  disjdsct  32796  f1od2  32812  hashxpe  32900  tosglblem  33054  mgcval  33067  pmtrprfv2  33169  elrgspnlem2  33324  ssdifidllem  33536  ssmxidllem  33553  ccfldextdgrr  33837  fldext2chn  33893  ordtconnlem1  34089  esumpfinvalf  34241  esum2dlem  34257  measiuns  34382  eulerpartlemt0  34534  eulerpartlemr  34539  eulerpartlemn  34546  ballotlem2  34654  ballotlemodife  34663  bnj887  34929  bnj976  34941  bnj1385  34995  bnj153  35043  bnj543  35056  bnj607  35079  bnj882  35089  bnj916  35096  bnj983  35114  axreg  35292  axregscl  35293  axregs  35304  derangenlem  35374  pconnconn  35434  fmlaomn0  35593  fmla0disjsuc  35601  fmlasucdisj  35602  elmpst  35739  xpab  35929  dftr6  35954  dffr5  35957  fundmpss  35970  elpotr  35982  brtxp  36081  brpprod  36086  brsset  36090  idsset  36091  dfon3  36093  ellimits  36111  dffun10  36115  elfuns  36116  brcart  36133  brimg  36138  brapply  36139  brcap  36141  lemsuccf  36142  funpartfun  36146  dfrecs2  36153  dfrdg4  36154  altopthc  36174  altopthd  36175  altopelaltxp  36179  outsideoftr  36332  rmoeqbii  36391  reueqbii  36393  rabeqbii  36397  riotaeqbii  36401  ixpeq1i  36403  cbvixpvw2  36448  cbvprodvw2  36450  trer  36519  neibastop1  36562  neifg  36574  df3nandALT1  36602  imnand2  36605  axtco  36674  regsfromregtco  36741  regsfromunir1  36743  eliminable-abelab  37190  bj-eldiag2  37504  bj-imdiridlem  37512  bj-opabco  37515  bj-xpcossxp  37516  topdifinfeq  37677  relowlssretop  37690  relowlpssretop  37691  wl-cases2-dnf  37848  poimirlem30  37982  poimirlem32  37984  ismblfin  37993  mbfposadd  37999  inixp  38060  elghomOLD  38219  keridl  38364  smprngopr  38384  sbcani  38440  inxpxrn  38750  dfcoss2  38835  cosscnv  38838  coss1cnvres  38839  coss2cnvepres  38840  1cossres  38851  dfcoels  38852  trressn  38867  br1cossinres  38869  br1cossinidres  38871  br1cossincnvepres  38872  br1cossxrnidres  38873  br1cossxrncnvepres  38874  cosscnvssid3  38898  coss0  38901  cossid  38902  trcoss  38904  eleccossin  38905  dfssr2  38911  br1cossxrncnvssrres  38920  refsymrels3  38982  refsymrel2  38983  refsymrel3  38984  elrefsymrels3  38986  dfeqvrel2  39006  dfeqvrel3  39007  redundeq1  39045  redundpbi1  39047  dfcomember3  39091  eqvreldmqs  39092  eqvreldmqs2  39093  dfeldisj3  39143  eldisjdmqsim  39149  eldisjn0elb  39177  antisymrelres  39198  dfmembpart2  39205  prtlem10  39322  prter1  39336  lcvbr3  39480  isopos  39637  llnexatN  39978  snatpsubN  40207  pclclN  40348  pclfinN  40357  lhpocnel2  40476  cdlemk19w  41429  dih1dimatlem  41786  psspwb  42680  redvmptabs  42803  mzpclall  43170  mzpincl  43177  mzpindd  43189  2nn0ind  43388  dford4  43472  wopprc  43473  islmodfg  43512  ifpan123g  43901  ifpan23  43902  ifpnot23  43920  ifpdfxor  43929  ifpidg  43933  ifpid1g  43936  ifpim23g  43937  ifpim123g  43942  ifpim1g  43943  ifp1bi  43944  ifpimimb  43946  ifpororb  43947  ifpor123g  43950  ifpbibib  43952  rp-isfinite6  43960  alephiso2  44000  undmrnresiss  44046  cotrintab  44056  brtrclfv2  44169  dfxor4  44208  snhesn  44228  dffrege76  44381  uneqsn  44467  expandan  44730  ismnuprim  44736  nzin  44760  onfrALTlem5  44984  onfrALTlem4  44985  undif3VD  45323  onfrALTlem5VD  45326  onfrALTlem4VD  45327  dfac5prim  45432  wfaxpr  45440  brpermmodel  45445  permac8prim  45456  ndisj2  45497  rexabsle  45862  ellimcabssub0  46062  limsupre2mpt  46173  limsupre3  46176  limsupre3mpt  46177  limsupre3uz  46179  limsupreuz  46180  liminfreuz  46246  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  smflim  47220  smflim2  47249  smflimsuplem1  47263  smflimsup  47271  cfsetsnfsetf1  47504  2reu8i  47558  ichan  47912  clnbgrsym  48311  dfnbgr6  48330  upgrimpthslem2  48381  isgrlim  48455  usgrexmpl2trifr  48510  pgnbgreunbgrlem5  48596  pgnbgreunbgr  48598  2zlidl  48713  islininds2  48957  zlmodzxzldeplem3  48975  2itscp  49254  reutruALT  49277  iinxp  49303  0funclem  49558  fucofulem2  49783  fuco2el  49784  catcinv  49871  2arwcatlem1  50067  alsi-no-surprise  50268