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  1501  cadan  1610  nic-axALT  1675  19.43OLD  1884  sbbi  2309  aaan  2333  sbnf2  2358  eubii  2580  cbveuvw  2600  cbveuw  2601  cbveuALT  2603  2mo2  2642  2eu4  2650  sbabel  2927  neanior  3021  r19.26m  3091  reeanlem  3203  rexeqbii  3311  reu5  3348  cbvreuw  3372  cgsex4g  3483  reu2  3679  reu3  3681  2reu5a  3698  2reu5lem3  3711  2reu1  3843  eqss  3945  unss  4137  ralunb  4144  ssin  4186  undi  4232  indifdi  4241  undif3  4247  inab  4256  difab  4257  reuss2  4273  reupick  4276  2reu4lem  4469  reuprg  4653  sstp  4785  tpss  4786  prneimg  4803  prneimg2  4804  prnebg  4805  uniin  4880  intun  4928  disjiun  5077  disjxiun  5086  brin  5141  brdif  5142  ssext  5393  pweqb  5395  opthg2  5417  copsex4g  5433  propeqop  5445  eqopab2bw  5486  eqopab2b  5490  pwin  5505  pofun  5540  dffr6  5570  wetrep  5607  elxp3  5680  soinxp  5696  weinxp  5699  csbxp  5715  relun  5750  inopab  5768  difopab  5769  inxp  5770  inxpOLD  5771  opelco2g  5806  cnvco  5824  dmin  5850  restidsing  6001  intasym  6061  asymref  6062  asymref2  6063  cnvdif  6090  xpnz  6106  difxp  6111  xpdifid  6115  xp11  6122  dfco2  6192  cnvpo  6234  cnvso  6235  xpco  6236  reu3op  6239  dfpo2  6243  dffun4  6494  funun  6527  fun11  6555  fununi  6556  imadif  6565  fnres  6608  mptfnf  6616  fnopabg  6618  fun  6685  fin  6703  dff1o2  6768  brprcneu  6812  brprcneuALT  6813  dffv2  6917  fsn  7068  f13dfv  7208  dff1o6  7209  isotr  7270  eqoprab2bw  7416  eqoprab2b  7417  fvmpopr2d  7508  porpss  7660  epweon  7708  onsucb  7747  resf1extb  7864  elxp6  7955  dfoprab3  7986  opiota  7991  poxp  8058  soxp  8059  poxp2  8073  xpord2pred  8075  xpord2indlem  8077  xpord3pred  8082  xpord3inddlem  8084  soseq  8089  suppvalbr  8094  brtpos2  8162  frrlem9  8224  fprlem1  8230  tfrlem7  8302  dfer2  8623  eqer  8658  iiner  8713  uniinqs  8721  brecop  8734  eroveu  8736  erovlem  8737  fsetexb  8788  mapval2  8796  ixpin  8847  boxriin  8864  brsdom  8897  xpcomco  8980  xpassen  8984  sbthlem9  9008  sbthlem10  9009  brsdom2  9014  ssenen  9064  sbthfilem  9107  dffi3  9315  dfsup2  9328  infcllem  9372  axinf2  9530  zfinf2  9532  oemapso  9572  ttrcltr  9606  frrlem15  9650  scottexs  9780  scott0s  9781  kardex  9787  karden  9788  dfac5lem1  10014  dfac5lem3  10016  kmlem15  10056  enfin2i  10212  fin23lem34  10237  brdom7disj  10422  fpwwe2lem11  10532  fpwwe2lem12  10533  axgroth5  10715  grothprim  10725  addsrpr  10966  mulsrpr  10967  mulgt0sr  10996  addcnsr  11026  mulcnsr  11027  ltresr  11031  axcnre  11055  ssxr  11182  infrenegsup  12105  nnwos  12813  zmin  12842  xrnemnf  13016  xrnepnf  13017  xmullem  13163  xmulcom  13165  xmulneg1  13168  xmulf  13171  xrinfmss2  13210  elfzuzb  13418  fzass4  13462  seqof  13966  hashbclem  14359  hashfacen  14361  xpcogend  14881  trclublem  14902  rexanre  15254  caubnd  15266  o1lo1  15444  rpnnen2lem12  16134  lcmcllem  16507  lcmftp  16547  lcmfunsnlem2  16551  isprm3  16594  prmreclem2  16829  4sqlem12  16868  catcone0  17593  isffth2  17825  fucinv  17883  lublecllem  18264  odulub  18311  oduglb  18313  issubmgm  18610  rabsubmgmd  18612  mndpsuppss  18673  issubm  18711  issubmd  18714  0subm  18725  insubm  18726  sursubmefmnd  18804  injsubmefmnd  18805  smndex1mgm  18815  isnsg2  19068  cycsubm  19114  oppgid  19268  symgfixf1  19349  pmtrrn2  19372  lsmdisjr  19596  lsmhash  19617  gsumcom3  19890  dprd0  19945  issrg  20106  dvdsrtr  20286  isirred2  20339  isdomn3  20630  opprdomnb  20632  isdomn4r  20634  lss1d  20896  lspsolvlem  21079  lbsextlem2  21096  cnfldfun  21305  cnfldfunOLD  21318  unocv  21617  iunocv  21618  evlsval  22021  mpomatmul  22361  cpmidpmat  22788  tgval2  22871  fctop  22919  ppttop  22922  epttop  22924  cnnei  23197  2ndcctbss  23370  txuni2  23480  txbas  23482  ptbasin  23492  txdis1cn  23550  xkococnlem  23574  opnfbas  23757  fgcl  23793  fbasrn  23799  filuni  23800  cfinfil  23808  csdfil  23809  fin1aufil  23847  rnelfmlem  23867  fmfnfmlem3  23871  txflf  23921  xmeterval  24347  reconn  24744  iimulcl  24860  isclmp  25024  iscau3  25205  rrxmvallem  25331  minveclem3  25356  pmltpc  25378  ovolfcl  25394  ismbl  25454  dyaddisj  25524  iblre  25722  plyun0  26129  logfaclbnd  27160  lgslem3  27237  lgsdir2lem5  27267  nosupinfsep  27671  sltrec  27762  madebdaylemlrcut  27844  addsproplem2  27913  addsuniflem  27944  negsproplem2  27971  negsid  27983  mulsproplem5  28059  mulsproplem6  28060  mulsproplem7  28061  mulsproplem8  28062  mulsproplem9  28063  mulsuniflem  28088  precsexlem9  28153  precsexlem10  28154  nnaddscl  28274  nnmulscl  28275  zaddscl  28318  zsoring  28332  recut  28398  0reno  28399  readdscl  28401  remulscl  28404  tgjustf  28451  ishpg  28737  usgrexmpllem  29238  nb3grpr2  29361  vtxd0nedgb  29467  wlk1walk  29617  clwlkcompbp  29760  wwlknllvtx  29824  wwlksonvtx  29833  wspthnonp  29837  wwlksn0s  29839  wwlksnndef  29883  2wlkdlem8  29911  elwwlks2s3  29929  clwwlkf1  30029  clwwlknonccat  30076  clwwlknon2x  30083  3pthdlem1  30144  upgr4cycl4dv4e  30165  frgr2wwlk1  30309  frgrreg  30374  ajfval  30789  issh  31188  chcon2i  31444  chcon3i  31446  spanuni  31524  5oalem7  31640  3oalem3  31644  pjin2i  32173  pjin3i  32174  cvnbtwn4  32269  mdslj1i  32299  mdslj2i  32300  mdslmd1i  32309  chrelat4i  32353  chirredi  32374  cdj3i  32421  rmoun  32473  difrab2  32477  eqdif  32499  inpr0  32512  iuninc  32540  fcoinvbr  32585  suppss2f  32620  fmptdF  32638  disjdsct  32684  f1od2  32702  hashxpe  32789  tosglblem  32955  mgcval  32968  pmtrprfv2  33057  elrgspnlem2  33210  ssdifidllem  33421  ssmxidllem  33438  ccfldextdgrr  33685  fldext2chn  33741  ordtconnlem1  33937  esumpfinvalf  34089  esum2dlem  34105  measiuns  34230  eulerpartlemt0  34382  eulerpartlemr  34387  eulerpartlemn  34394  ballotlem2  34502  ballotlemodife  34511  bnj887  34777  bnj976  34789  bnj1385  34844  bnj153  34892  bnj543  34905  bnj607  34928  bnj882  34938  bnj916  34945  bnj983  34963  axreg  35125  axregscl  35126  axregs  35145  derangenlem  35215  pconnconn  35275  fmlaomn0  35434  fmla0disjsuc  35442  fmlasucdisj  35443  elmpst  35580  xpab  35770  dftr6  35795  dffr5  35798  fundmpss  35811  elpotr  35823  brtxp  35922  brpprod  35927  brsset  35931  idsset  35932  dfon3  35934  ellimits  35952  dffun10  35956  elfuns  35957  brcart  35974  brimg  35979  brapply  35980  brcap  35982  lemsuccf  35983  funpartfun  35987  dfrecs2  35994  dfrdg4  35995  altopthc  36015  altopthd  36016  altopelaltxp  36020  outsideoftr  36173  rmoeqbii  36232  reueqbii  36234  rabeqbii  36238  riotaeqbii  36242  ixpeq1i  36244  cbvixpvw2  36289  cbvprodvw2  36291  trer  36360  neibastop1  36403  neifg  36415  df3nandALT1  36443  imnand2  36446  eliminable-abelab  36914  bj-eldiag2  37221  bj-imdiridlem  37229  bj-opabco  37232  bj-xpcossxp  37233  topdifinfeq  37394  relowlssretop  37407  relowlpssretop  37408  wl-cases2-dnf  37556  poimirlem30  37700  poimirlem32  37702  ismblfin  37711  mbfposadd  37717  inixp  37778  elghomOLD  37937  keridl  38082  smprngopr  38102  sbcani  38158  inxpxrn  38452  dfcoss2  38525  cosscnv  38528  coss1cnvres  38529  coss2cnvepres  38530  1cossres  38541  dfcoels  38542  trressn  38557  br1cossinres  38559  br1cossinidres  38561  br1cossincnvepres  38562  br1cossxrnidres  38563  br1cossxrncnvepres  38564  cosscnvssid3  38588  coss0  38591  cossid  38592  trcoss  38594  eleccossin  38595  dfssr2  38601  br1cossxrncnvssrres  38610  refsymrels3  38672  refsymrel2  38673  refsymrel3  38674  elrefsymrels3  38676  dfeqvrel2  38696  dfeqvrel3  38697  redundeq1  38735  redundpbi1  38737  dfcomember3  38782  eqvreldmqs  38783  eqvreldmqs2  38784  dfeldisj3  38827  eldisjn0elb  38853  antisymrelres  38871  dfmembpart2  38878  prtlem10  38974  prter1  38988  lcvbr3  39132  isopos  39289  llnexatN  39630  snatpsubN  39859  pclclN  40000  pclfinN  40009  lhpocnel2  40128  cdlemk19w  41081  dih1dimatlem  41438  psspwb  42331  redvmptabs  42463  mzpclall  42830  mzpincl  42837  mzpindd  42849  2nn0ind  43048  dford4  43132  wopprc  43133  islmodfg  43172  ifpan123g  43562  ifpan23  43563  ifpnot23  43581  ifpdfxor  43590  ifpidg  43594  ifpid1g  43597  ifpim23g  43598  ifpim123g  43603  ifpim1g  43604  ifp1bi  43605  ifpimimb  43607  ifpororb  43608  ifpor123g  43611  ifpbibib  43613  rp-isfinite6  43621  alephiso2  43661  undmrnresiss  43707  cotrintab  43717  brtrclfv2  43830  dfxor4  43869  snhesn  43889  dffrege76  44042  uneqsn  44128  expandan  44391  ismnuprim  44397  nzin  44421  onfrALTlem5  44645  onfrALTlem4  44646  undif3VD  44984  onfrALTlem5VD  44987  onfrALTlem4VD  44988  dfac5prim  45093  wfaxpr  45101  brpermmodel  45106  permac8prim  45117  ndisj2  45158  rexabsle  45527  ellimcabssub0  45727  limsupre2mpt  45838  limsupre3  45841  limsupre3mpt  45842  limsupre3uz  45844  limsupreuz  45845  liminfreuz  45911  fourierdlem103  46317  fourierdlem104  46318  fourierdlem112  46326  smflim  46885  smflim2  46914  smflimsuplem1  46928  smflimsup  46936  cfsetsnfsetf1  47169  2reu8i  47223  ichan  47565  clnbgrsym  47948  dfnbgr6  47967  upgrimpthslem2  48018  isgrlim  48092  usgrexmpl2trifr  48147  pgnbgreunbgrlem5  48233  pgnbgreunbgr  48235  2zlidl  48350  islininds2  48595  zlmodzxzldeplem3  48613  2itscp  48892  reutruALT  48915  iinxp  48941  0funclem  49197  fucofulem2  49422  fuco2el  49423  catcinv  49510  2arwcatlem1  49706  alsi-no-surprise  49907