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  2313  aaan  2337  sbnf2  2362  cbveuvw  2605  cbveuw  2606  cbveuALT  2608  2mo2  2647  2eu4  2655  sbabel  2931  neanior  3025  r19.26m  3095  reeanlem  3207  rexeqbii  3315  reu5  3352  cbvreuw  3376  cgsex4g  3487  reu2  3683  reu3  3685  2reu5a  3702  2reu5lem3  3715  2reu1  3847  eqss  3949  unss  4142  ralunb  4149  ssin  4191  undi  4237  indifdi  4246  undif3  4252  inab  4261  difab  4262  reuss2  4278  reupick  4281  2reu4lem  4476  reuprg  4660  sstp  4792  tpss  4793  prneimg  4810  prneimg2  4811  prnebg  4812  uniin  4887  intun  4935  disjiun  5086  disjxiun  5095  brin  5150  brdif  5151  ssext  5402  pweqb  5404  opthg2  5427  copsex4g  5443  propeqop  5455  eqopab2bw  5496  eqopab2b  5500  pwin  5515  pofun  5550  dffr6  5580  wetrep  5617  elxp3  5690  soinxp  5706  weinxp  5709  csbxp  5725  relun  5760  inopab  5778  difopab  5779  inxp  5780  inxpOLD  5781  opelco2g  5816  cnvco  5834  dmin  5860  restidsing  6012  intasym  6072  asymref  6073  asymref2  6074  cnvdif  6101  xpnz  6117  difxp  6122  xpdifid  6126  xp11  6133  dfco2  6203  cnvpo  6245  cnvso  6246  xpco  6247  reu3op  6250  dfpo2  6254  dffun4  6505  funun  6538  fun11  6566  fununi  6567  imadif  6576  fnres  6619  mptfnf  6627  fnopabg  6629  fun  6696  fin  6714  dff1o2  6779  brprcneu  6824  brprcneuALT  6825  dffv2  6929  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  8070  soxp  8071  poxp2  8085  xpord2pred  8087  xpord2indlem  8089  xpord3pred  8094  xpord3inddlem  8096  soseq  8101  suppvalbr  8106  brtpos2  8174  frrlem9  8236  fprlem1  8242  tfrlem7  8314  dfer2  8636  eqer  8671  iiner  8726  uniinqs  8734  brecop  8747  eroveu  8749  erovlem  8750  fsetexb  8801  mapval2  8810  ixpin  8861  boxriin  8878  brsdom  8911  xpcomco  8995  xpassen  8999  sbthlem9  9023  sbthlem10  9024  brsdom2  9029  ssenen  9079  sbthfilem  9122  dffi3  9334  dfsup2  9347  infcllem  9391  axinf2  9549  zfinf2  9551  oemapso  9591  ttrcltr  9625  frrlem15  9669  scottexs  9799  scott0s  9800  kardex  9806  karden  9807  dfac5lem1  10033  dfac5lem3  10035  kmlem15  10075  enfin2i  10231  fin23lem34  10256  brdom7disj  10441  fpwwe2lem11  10552  fpwwe2lem12  10553  axgroth5  10735  grothprim  10745  addsrpr  10986  mulsrpr  10987  mulgt0sr  11016  addcnsr  11046  mulcnsr  11047  ltresr  11051  axcnre  11075  ssxr  11202  infrenegsup  12125  nnwos  12828  zmin  12857  xrnemnf  13031  xrnepnf  13032  xmullem  13179  xmulcom  13181  xmulneg1  13184  xmulf  13187  xrinfmss2  13226  elfzuzb  13434  fzass4  13478  seqof  13982  hashbclem  14375  hashfacen  14377  xpcogend  14897  trclublem  14918  rexanre  15270  caubnd  15282  o1lo1  15460  rpnnen2lem12  16150  lcmcllem  16523  lcmftp  16563  lcmfunsnlem2  16567  isprm3  16610  prmreclem2  16845  4sqlem12  16884  catcone0  17610  isffth2  17842  fucinv  17900  lublecllem  18281  odulub  18328  oduglb  18330  issubmgm  18627  rabsubmgmd  18629  mndpsuppss  18690  issubm  18728  issubmd  18731  0subm  18742  insubm  18743  sursubmefmnd  18821  injsubmefmnd  18822  smndex1mgm  18832  isnsg2  19085  cycsubm  19131  oppgid  19285  symgfixf1  19366  pmtrrn2  19389  lsmdisjr  19613  lsmhash  19634  gsumcom3  19907  dprd0  19962  issrg  20123  dvdsrtr  20304  isirred2  20357  isdomn3  20648  opprdomnb  20650  isdomn4r  20652  lss1d  20914  lspsolvlem  21097  lbsextlem2  21114  cnfldfun  21323  cnfldfunOLD  21336  unocv  21635  iunocv  21636  evlsval  22041  mpomatmul  22390  cpmidpmat  22817  tgval2  22900  fctop  22948  ppttop  22951  epttop  22953  cnnei  23226  2ndcctbss  23399  txuni2  23509  txbas  23511  ptbasin  23521  txdis1cn  23579  xkococnlem  23603  opnfbas  23786  fgcl  23822  fbasrn  23828  filuni  23829  cfinfil  23837  csdfil  23838  fin1aufil  23876  rnelfmlem  23896  fmfnfmlem3  23900  txflf  23950  xmeterval  24376  reconn  24773  iimulcl  24889  isclmp  25053  iscau3  25234  rrxmvallem  25360  minveclem3  25385  pmltpc  25407  ovolfcl  25423  ismbl  25483  dyaddisj  25553  iblre  25751  plyun0  26158  logfaclbnd  27189  lgslem3  27266  lgsdir2lem5  27296  nosupinfsep  27700  ltsrec  27797  madebdaylemlrcut  27895  addsproplem2  27966  addsuniflem  27997  negsproplem2  28025  negsid  28037  mulsproplem5  28116  mulsproplem6  28117  mulsproplem7  28118  mulsproplem8  28119  mulsproplem9  28120  mulsuniflem  28145  precsexlem9  28211  precsexlem10  28212  ons2ind  28271  nnaddscl  28342  nnmulscl  28343  zaddscl  28390  zsoring  28405  recut  28490  readdscl  28495  remulscl  28498  tgjustf  28545  ishpg  28831  usgrexmpllem  29333  nb3grpr2  29456  vtxd0nedgb  29562  wlk1walk  29712  clwlkcompbp  29855  wwlknllvtx  29919  wwlksonvtx  29928  wspthnonp  29932  wwlksn0s  29934  wwlksnndef  29978  2wlkdlem8  30006  elwwlks2s3  30024  clwwlkf1  30124  clwwlknonccat  30171  clwwlknon2x  30178  3pthdlem1  30239  upgr4cycl4dv4e  30260  frgr2wwlk1  30404  frgrreg  30469  ajfval  30884  issh  31283  chcon2i  31539  chcon3i  31541  spanuni  31619  5oalem7  31735  3oalem3  31739  pjin2i  32268  pjin3i  32269  cvnbtwn4  32364  mdslj1i  32394  mdslj2i  32395  mdslmd1i  32404  chrelat4i  32448  chirredi  32469  cdj3i  32516  rmoun  32568  difrab2  32572  eqdif  32594  inpr0  32607  iuninc  32635  fcoinvbr  32680  suppss2f  32716  fmptdF  32734  disjdsct  32782  f1od2  32798  hashxpe  32887  tosglblem  33056  mgcval  33069  pmtrprfv2  33170  elrgspnlem2  33325  ssdifidllem  33537  ssmxidllem  33554  ccfldextdgrr  33829  fldext2chn  33885  ordtconnlem1  34081  esumpfinvalf  34233  esum2dlem  34249  measiuns  34374  eulerpartlemt0  34526  eulerpartlemr  34531  eulerpartlemn  34538  ballotlem2  34646  ballotlemodife  34655  bnj887  34921  bnj976  34933  bnj1385  34988  bnj153  35036  bnj543  35049  bnj607  35072  bnj882  35082  bnj916  35089  bnj983  35107  axreg  35283  axregscl  35284  axregs  35295  derangenlem  35365  pconnconn  35425  fmlaomn0  35584  fmla0disjsuc  35592  fmlasucdisj  35593  elmpst  35730  xpab  35920  dftr6  35945  dffr5  35948  fundmpss  35961  elpotr  35973  brtxp  36072  brpprod  36077  brsset  36081  idsset  36082  dfon3  36084  ellimits  36102  dffun10  36106  elfuns  36107  brcart  36124  brimg  36129  brapply  36130  brcap  36132  lemsuccf  36133  funpartfun  36137  dfrecs2  36144  dfrdg4  36145  altopthc  36165  altopthd  36166  altopelaltxp  36170  outsideoftr  36323  rmoeqbii  36382  reueqbii  36384  rabeqbii  36388  riotaeqbii  36392  ixpeq1i  36394  cbvixpvw2  36439  cbvprodvw2  36441  trer  36510  neibastop1  36553  neifg  36565  df3nandALT1  36593  imnand2  36596  regsfromregtr  36668  regsfromunir1  36670  eliminable-abelab  37071  bj-eldiag2  37382  bj-imdiridlem  37390  bj-opabco  37393  bj-xpcossxp  37394  topdifinfeq  37555  relowlssretop  37568  relowlpssretop  37569  wl-cases2-dnf  37717  poimirlem30  37851  poimirlem32  37853  ismblfin  37862  mbfposadd  37868  inixp  37929  elghomOLD  38088  keridl  38233  smprngopr  38253  sbcani  38309  inxpxrn  38613  dfcoss2  38686  cosscnv  38689  coss1cnvres  38690  coss2cnvepres  38691  1cossres  38702  dfcoels  38703  trressn  38718  br1cossinres  38720  br1cossinidres  38722  br1cossincnvepres  38723  br1cossxrnidres  38724  br1cossxrncnvepres  38725  cosscnvssid3  38749  coss0  38752  cossid  38753  trcoss  38755  eleccossin  38756  dfssr2  38762  br1cossxrncnvssrres  38771  refsymrels3  38833  refsymrel2  38834  refsymrel3  38835  elrefsymrels3  38837  dfeqvrel2  38857  dfeqvrel3  38858  redundeq1  38896  redundpbi1  38898  dfcomember3  38943  eqvreldmqs  38944  eqvreldmqs2  38945  dfeldisj3  38988  eldisjn0elb  39014  antisymrelres  39032  dfmembpart2  39039  prtlem10  39135  prter1  39149  lcvbr3  39293  isopos  39450  llnexatN  39791  snatpsubN  40020  pclclN  40161  pclfinN  40170  lhpocnel2  40289  cdlemk19w  41242  dih1dimatlem  41599  psspwb  42494  redvmptabs  42625  mzpclall  42979  mzpincl  42986  mzpindd  42998  2nn0ind  43197  dford4  43281  wopprc  43282  islmodfg  43321  ifpan123g  43710  ifpan23  43711  ifpnot23  43729  ifpdfxor  43738  ifpidg  43742  ifpid1g  43745  ifpim23g  43746  ifpim123g  43751  ifpim1g  43752  ifp1bi  43753  ifpimimb  43755  ifpororb  43756  ifpor123g  43759  ifpbibib  43761  rp-isfinite6  43769  alephiso2  43809  undmrnresiss  43855  cotrintab  43865  brtrclfv2  43978  dfxor4  44017  snhesn  44037  dffrege76  44190  uneqsn  44276  expandan  44539  ismnuprim  44545  nzin  44569  onfrALTlem5  44793  onfrALTlem4  44794  undif3VD  45132  onfrALTlem5VD  45135  onfrALTlem4VD  45136  dfac5prim  45241  wfaxpr  45249  brpermmodel  45254  permac8prim  45265  ndisj2  45306  rexabsle  45673  ellimcabssub0  45873  limsupre2mpt  45984  limsupre3  45987  limsupre3mpt  45988  limsupre3uz  45990  limsupreuz  45991  liminfreuz  46057  fourierdlem103  46463  fourierdlem104  46464  fourierdlem112  46472  smflim  47031  smflim2  47060  smflimsuplem1  47074  smflimsup  47082  cfsetsnfsetf1  47315  2reu8i  47369  ichan  47711  clnbgrsym  48094  dfnbgr6  48113  upgrimpthslem2  48164  isgrlim  48238  usgrexmpl2trifr  48293  pgnbgreunbgrlem5  48379  pgnbgreunbgr  48381  2zlidl  48496  islininds2  48740  zlmodzxzldeplem3  48758  2itscp  49037  reutruALT  49060  iinxp  49086  0funclem  49341  fucofulem2  49566  fuco2el  49567  catcinv  49654  2arwcatlem1  49850  alsi-no-surprise  50051