Theorem anbi12i 640

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 635	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜃))
3		anbi12.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	bianbi 639	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi12ci  641  an2anr  648  ordi  1023  ordir  1024  orddi  1027  pm5.17  1029  xor  1032  cases2  1063  3anbi123i  1173  an6  1474  nanbi  1529  cadan  1641  nic-axALT  1706  19.43OLD  1917  sbbi  2343  aaan  2365  sbnf2  2390  cbveuvw  2633  cbveuw  2634  cbveuALT  2636  2mo2  2675  2eu4  2682  sbabel  2958  neanior  3052  r19.26m  3125  reeanlem  3237  rexeqbii  3337  reu5  3371  cbvreuw  3395  cgsex4g  3500  reu2  3686  reu3  3688  2reu5a  3705  2reu5lem3  3718  2reu1  3849  eqss  3928  ssin  4138  unss  4191  ralunb  4198  undi  4233  indifdi  4242  undif3  4248  inab  4257  difab  4258  reuss2  4274  reupick  4277  2reu4lem  4482  reuprg  4664  sstp  4794  tpss  4795  prneimg  4812  prneimg2  4813  prnebg  4814  uniinOLD  4895  intun  4943  disjiun  5094  disjxiun  5103  brin  5160  brdif  5161  ssext  5426  pweqb  5428  opthg2  5452  copsex4g  5471  propeqop  5483  eqopab2bw  5527  eqopab2b  5531  pwin  5546  pofun  5581  dffr6  5611  wetrep  5648  elxp3  5721  soinxp  5738  weinxp  5741  csbxp  5757  relun  5794  inopab  5812  difopab  5813  inxp  5814  opelco2g  5850  cnvco  5872  dmin  5898  restidsing  6051  intasym  6115  asymref  6116  asymref2  6117  cnvdif  6140  xpnz  6156  difxp  6161  xpdifid  6165  xpdifcnvepel  6166  xp11  6173  dfco2  6253  cnvpo  6297  cnvso  6298  xpco  6299  reu3op  6302  dfpo2  6306  dffun4  6560  funun  6595  fun11  6625  fununi  6626  imadif  6635  fnres  6677  mptfnf  6685  fnopabg  6687  fun  6755  fin  6773  dff1o2  6841  brprcneu  6886  brprcneuALT  6887  dffv2  6991  fsn  7147  f13dfv  7292  dff1o6  7293  isotr  7354  eqoprab2bw  7500  eqoprab2b  7501  fvmpopr2d  7592  porpss  7753  epweon  7799  onsucb  7838  resf1extb  7956  elxp6  8045  dfoprab3  8076  opiota  8081  f1od2  8121  poxp  8153  soxp  8154  poxp2  8173  xpord2pred  8175  xpord2indlem  8177  xpord3pred  8182  xpord3inddlem  8184  soseq  8189  suppvalbr  8194  suppvalbrOLD  8195  brtpos2  8263  frrlem9  8326  fprlem1  8332  tfrlem7  8405  dfer2  8732  eqer  8768  iiner  8824  uniinqs  8832  brecop  8845  eroveu  8847  erovlem  8848  fsetexb  8900  mapval2  8914  ixpin  8965  boxriin  8982  brsdom  9015  xpcomco  9100  xpassen  9104  sbthlem9  9128  sbthlem10  9129  brsdom2  9134  ssenen  9184  sbthfilem  9227  dffi3  9436  dfsup2  9449  infcllem  9493  axinf2  9654  zfinf2  9656  oemapso  9696  ttrcltr  9730  frrlem15  9774  scottexsOLD  9956  scott0bsOLD  9958  kardexOLD  9971  kardenOLD  9973  dfac5lem1  10215  dfac5lem3  10217  kmlem15  10256  enfin2i  10412  fin23lem34  10437  brdom7disj  10623  fpwwe2lem11  10739  fpwwe2lem12  10740  axgroth5  10922  grothprim  10932  addsrpr  11173  mulsrpr  11174  mulgt0sr  11203  addcnsr  11233  mulcnsr  11234  ltresr  11238  axcnre  11262  ssxr  11392  infrenegsup  12313  nnwos  13055  zmin  13084  xrnemnf  13259  xrnepnf  13260  xmullem  13407  xmulcom  13409  xmulneg1  13412  xmulf  13415  xrinfmss2  13454  elfzuzb  13663  fzass4  13709  seqof  14215  hashbclem  14610  hashfacen  14612  xpcogend  15142  trclublem  15163  rexanre  15529  caubnd  15541  o1lo1  15719  rpnnen2lem12  16408  lcmcllem  16786  lcmftp  16826  lcmfunsnlem2  16830  isprm3  16873  prmreclem2  17110  4sqlem12  17149  catcone0  17876  isffth2  18108  fucinv  18166  lublecllem  18547  odulub  18594  oduglb  18596  issubmgm  18906  rabsubmgmd  18908  mndpsuppss  18974  issubm  19013  issubmd  19016  0subm  19028  insubm  19029  sursubmefmnd  19107  injsubmefmnd  19108  smndex1mgm  19121  degenmgm  19152  degenmgm2  19155  isnsg2  19381  cycsubm  19432  oppgid  19585  symgfixf1  19666  pmtrrn2  19689  lsmdisjr  19913  lsmhash  19934  gsumcom3  20207  dprd0  20262  issrg  20429  dvdsrtr  20613  isirred2  20666  isdomn3  20981  opprdomnb  20983  isdomn4r  20985  lss1d  21253  lspsolvlem  21435  lbsextlem2  21452  ssdifidllem  21655  cnfldfun  21707  unocv  22001  iunocv  22002  evlsval  22410  mpomatmul  22776  cpmidpmat  23206  tgval2  23289  fctop  23337  ppttop  23340  epttop  23342  cnnei  23615  2ndcctbss  23789  txuni2  23899  txbas  23901  ptbasin  23911  txdis1cn  23969  xkococnlem  23993  opnfbas  24176  fgcl  24212  fbasrn  24218  filuni  24219  cfinfil  24227  csdfil  24228  fin1aufil  24266  rnelfmlem  24286  fmfnfmlem3  24290  txflf  24340  xmeterval  24766  reconn  25163  iimulcl  25273  isclmp  25433  iscau3  25614  rrxmvallem  25740  minveclem3  25765  pmltpc  25786  ovolfcl  25802  ismbl  25862  dyaddisj  25932  iblre  26129  plyun0  26530  logfaclbnd  27564  lgslem3  27641  lgsdir2lem5  27671  nosupinfsep  28104  ltsrec  28202  madebdaylemlrcut  28300  addsproplem2  28371  addsuniflem  28402  negsproplem2  28430  negsid  28442  mulsproplem5  28521  mulsproplem6  28522  mulsproplem7  28523  mulsproplem8  28524  mulsproplem9  28525  mulsuniflem  28550  precsexlem9  28616  precsexlem10  28617  ons2ind  28676  nnaddscl  28747  nnmulscl  28748  zaddscl  28795  zsoring  28810  recut  28895  readdscl  28900  remulscl  28903  tgjustf  28950  ishpg  29252  usgrexmpllem  29856  nb3grpr2  29979  vtxd0nedgb  30084  wlk1walk  30234  clwlkcompbp  30384  wwlknllvtx  30450  wwlksonvtx  30459  wspthnonp  30463  wwlksn0s  30465  wwlksnndef  30509  2wlkdlem8  30537  elwwlks2s3  30555  clwwlkf1  30655  clwwlknonccat  30702  clwwlknon2x  30709  3pthdlem1  30780  upgr4cycl4dv4e  30801  frgr2wwlk1  30945  frgrreg  31010  ajfval  31426  issh  31825  chcon2i  32081  chcon3i  32083  spanuni  32161  5oalem7  32277  3oalem3  32281  pjin2i  32810  pjin3i  32811  cvnbtwn4  32906  mdslj1i  32936  mdslj2i  32937  mdslmd1i  32946  chrelat4i  32990  chirredi  33011  cdj3i  33058  rmoun  33147  difrab2  33151  eqdif  33172  inpr0  33185  iuninc  33212  fcoinvbr  33256  suppss2f  33289  fmptdf2  33307  disjdsct  33353  hashxpe  33455  tosglblem  33591  mgcval  33604  pmtrprfv2  33705  elrgspnlem2  33860  ssmxidllem  34054  ccfldextdgrr  34360  fldext2chn  34416  ordtconnlem1  34612  esumpfinvalf  34764  esum2dlem  34780  measiuns  34906  eulerpartlemt0  35057  eulerpartlemr  35062  eulerpartlemn  35069  ballotlem2  35177  ballotlemodife  35186  bnj887  35452  bnj976  35464  bnj1385  35518  bnj153  35566  bnj543  35579  bnj607  35602  bnj882  35612  bnj916  35619  bnj983  35637  axreg  35869  axregscl  35870  axregs  35881  onvfowev  36007  derangenlem  36060  pconnconn  36120  fmlaomn0  36279  fmla0disjsuc  36287  fmlasucdisj  36288  elmpst  36425  xpab  36621  dftr6  36646  dffr5  36649  fundmpss  36662  elpotr  36673  brtxp  36772  brpprod  36777  brsset  36781  idsset  36782  dfon3  36784  ellimits  36802  dffun10  36806  elfuns  36807  brcart  36824  brimg  36829  brapply  36830  brcap  36832  lemsuccf  36833  funpartfun  36837  dfrecs2  36844  dfrdg4  36845  altopthc  36866  altopthd  36867  altopelaltxp  36871  outsideoftr  37024  rmoeqbii  37107  reueqbii  37109  rabeqbii  37113  riotaeqbii  37117  ixpeq1i  37119  cbvixpvw2  37164  cbvprodvw2  37166  trer  37234  neibastop1  37277  neifg  37289  df3nandALT1  37317  imnand2  37320  axtco  37389  regsfromregtco  37456  regsfromunir1  37458  mh-prprimbi  37461  eliminable-abelab  37912  bj-eldiag2  38241  bj-imdiridlem  38249  bj-opabco  38252  bj-xpcossxp  38253  topdifinfeq  38416  relowlssretop  38429  relowlpssretop  38430  wl-cases2-dnf  38587  poimirlem30  38711  poimirlem32  38713  ismblfin  38722  mbfposadd  38728  inixp  38805  elghomOLD  38964  keridl  39109  smprngopr  39129  sbcani  39183  inxpxrn  39493  dfcoss2  39578  cosscnv  39581  coss1cnvres  39582  coss2cnvepres  39583  1cossres  39594  dfcoels  39595  trressn  39610  br1cossinres  39612  br1cossinidres  39614  br1cossincnvepres  39615  br1cossxrnidres  39616  br1cossxrncnvepres  39617  cosscnvssid3  39641  coss0  39644  cossid  39645  trcoss  39647  eleccossin  39648  dfssr2  39654  br1cossxrncnvssrres  39663  refsymrels3  39725  refsymrel2  39726  refsymrel3  39727  elrefsymrels3  39729  dfeqvrel2  39749  dfeqvrel3  39750  redundeq1  39788  redundpbi1  39790  dfcomember3  39834  eqvreldmqs  39835  eqvreldmqs2  39836  dfeldisj3  39886  eldisjdmqsim  39892  eldisjn0elb  39920  antisymrelres  39941  dfmembpart2  39948  prtlem10  40065  prter1  40079  lcvbr3  40223  isopos  40380  llnexatN  40721  snatpsubN  40950  pclclN  41091  pclfinN  41100  lhpocnel2  41219  cdlemk19w  42172  dih1dimatlem  42529  psspwb  43425  redvmptabs  43554  mzpclall  43881  mzpincl  43888  mzpindd  43900  2nn0ind  44095  dford4  44179  wopprc  44180  islmodfg  44214  ifpan123g  44603  ifpan23  44604  ifpnot23  44622  ifpdfxor  44631  ifpidg  44635  ifpid1g  44638  ifpim23g  44639  ifpim123g  44644  ifpim1g  44645  ifp1bi  44646  ifpimimb  44648  ifpororb  44649  ifpor123g  44652  ifpbibib  44654  rp-isfinite6  44662  alephiso2  44702  undmrnresiss  44747  cotrintab  44757  brtrclfv2  44870  dfxor4  44909  snhesn  44929  dffrege76  45082  uneqsn  45168  expandan  45415  ismnuprim  45421  nzin  45445  onfrALTlem5  45667  onfrALTlem4  45668  undif3VD  46006  onfrALTlem5VD  46009  onfrALTlem4VD  46010  dfac5prim  46122  wfaxpr  46130  brpermmodel  46135  permac8prim  46146  ndisj2  46210  rexabsle  46571  ellimcabssub0  46771  limsupre2mpt  46882  limsupre3  46885  limsupre3mpt  46886  limsupre3uz  46888  limsupreuz  46889  liminfreuz  46955  fourierdlem103  47361  fourierdlem104  47362  fourierdlem112  47370  smflim  47929  smflim2  47958  smflimsuplem1  47972  smflimsup  47980  cfsetsnfsetf1  48271  2reu8i  48326  ichan  48679  clnbgrsym  49078  dfnbgr6  49097  upgrimpthslem2  49148  isgrlim  49222  usgrexmpl2trifr  49277  pgnbgreunbgrlem5  49363  pgnbgreunbgr  49365  2zlidl  49479  smprngprmrng  49578  islininds2  49738  zlmodzxzldeplem3  49756  rrx2xpref1o  49973  2itscp  50035  reutruALT  50057  iinxp  50084  0funclem  50343  fucofulem2  50575  fuco2el  50576  catcinv  50676  2arwcatlem1  50875  dfrals2  51103  alsbii  51113  ralsbii  51114  cbvals  51118  als-no-surprise  51119  rals-no-surprise  51120  dfralseu2  51136  alseubii  51145  ralseubii  51146