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  1500  cadan  1609  nic-axALT  1674  19.43OLD  1883  sbbi  2307  aaan  2331  sbnf2  2356  eubii  2578  cbveuvw  2598  cbveuw  2599  cbveuALT  2601  2mo2  2640  2eu4  2648  sbabel  2924  neanior  3018  r19.26m  3090  reeanlem  3206  rexeqbii  3315  reu5  3353  cbvreuw  3379  cgsex4g  3491  reu2  3693  reu3  3695  2reu5a  3712  2reu5lem3  3725  2reu1  3857  eqss  3959  unss  4149  ralunb  4156  ssin  4198  undi  4244  indifdi  4253  undif3  4259  inab  4268  difab  4269  reuss2  4285  reupick  4288  2reu4lem  4481  reuprg  4663  sstp  4796  tpss  4797  prneimg  4814  prneimg2  4815  prnebg  4816  uniin  4891  intun  4940  disjiun  5090  disjxiun  5099  brin  5154  brdif  5155  ssext  5409  pweqb  5411  opthg2  5434  copsex4g  5450  propeqop  5462  eqopab2bw  5503  eqopab2b  5507  pwin  5522  pofun  5557  dffr6  5587  wetrep  5624  elxp3  5697  soinxp  5713  weinxp  5716  csbxp  5730  relun  5765  inopab  5783  difopab  5784  inxp  5785  inxpOLD  5786  opelco2g  5821  cnvco  5839  dmin  5865  restidsing  6013  intasym  6076  asymref  6077  asymref2  6078  cnvdif  6104  xpnz  6120  difxp  6125  xpdifid  6129  xp11  6136  dfco2  6206  relssdmrnOLD  6230  cnvpo  6248  cnvso  6249  xpco  6250  reu3op  6253  dfpo2  6257  dffun4  6513  funun  6546  fun11  6574  fununi  6575  imadif  6584  fnres  6627  mptfnf  6635  fnopabg  6637  fun  6704  fin  6722  dff1o2  6787  brprcneu  6830  brprcneuALT  6831  dffv2  6938  fsn  7089  f13dfv  7231  dff1o6  7232  isotr  7293  eqoprab2bw  7439  eqoprab2b  7440  fvmpopr2d  7531  porpss  7683  epweon  7731  onsucb  7772  resf1extb  7890  elxp6  7981  dfoprab3  8012  opiota  8017  poxp  8084  soxp  8085  poxp2  8099  xpord2pred  8101  xpord2indlem  8103  xpord3pred  8108  xpord3inddlem  8110  soseq  8115  suppvalbr  8120  brtpos2  8188  frrlem9  8250  fprlem1  8256  tfrlem7  8328  dfer2  8649  eqer  8684  iiner  8739  uniinqs  8747  brecop  8760  eroveu  8762  erovlem  8763  fsetexb  8814  mapval2  8822  ixpin  8873  boxriin  8890  brsdom  8923  xpcomco  9008  xpassen  9012  sbthlem9  9036  sbthlem10  9037  brsdom2  9042  ssenen  9092  sbthfilem  9139  dffi3  9358  dfsup2  9371  infcllem  9415  axinf2  9569  zfinf2  9571  oemapso  9611  ttrcltr  9645  frrlem15  9686  scottexs  9816  scott0s  9817  kardex  9823  karden  9824  dfac5lem1  10052  dfac5lem3  10054  kmlem15  10094  enfin2i  10250  fin23lem34  10275  brdom7disj  10460  fpwwe2lem11  10570  fpwwe2lem12  10571  axgroth5  10753  grothprim  10763  addsrpr  11004  mulsrpr  11005  mulgt0sr  11034  addcnsr  11064  mulcnsr  11065  ltresr  11069  axcnre  11093  ssxr  11219  infrenegsup  12142  nnwos  12850  zmin  12879  xrnemnf  13053  xrnepnf  13054  xmullem  13200  xmulcom  13202  xmulneg1  13205  xmulf  13208  xrinfmss2  13247  elfzuzb  13455  fzass4  13499  seqof  14000  hashbclem  14393  hashfacen  14395  xpcogend  14916  trclublem  14937  rexanre  15289  caubnd  15301  o1lo1  15479  rpnnen2lem12  16169  lcmcllem  16542  lcmftp  16582  lcmfunsnlem2  16586  isprm3  16629  prmreclem2  16864  4sqlem12  16903  catcone0  17628  isffth2  17860  fucinv  17918  lublecllem  18299  odulub  18346  oduglb  18348  issubmgm  18611  rabsubmgmd  18613  mndpsuppss  18674  issubm  18712  issubmd  18715  0subm  18726  insubm  18727  sursubmefmnd  18805  injsubmefmnd  18806  smndex1mgm  18816  isnsg2  19070  cycsubm  19116  oppgid  19270  symgfixf1  19351  pmtrrn2  19374  lsmdisjr  19598  lsmhash  19619  gsumcom3  19892  dprd0  19947  issrg  20108  dvdsrtr  20288  isirred2  20341  isdomn3  20635  opprdomnb  20637  isdomn4r  20639  lss1d  20901  lspsolvlem  21084  lbsextlem2  21101  cnfldfun  21310  cnfldfunOLD  21323  unocv  21622  iunocv  21623  evlsval  22026  mpomatmul  22366  cpmidpmat  22793  tgval2  22876  fctop  22924  ppttop  22927  epttop  22929  cnnei  23202  2ndcctbss  23375  txuni2  23485  txbas  23487  ptbasin  23497  txdis1cn  23555  xkococnlem  23579  opnfbas  23762  fgcl  23798  fbasrn  23804  filuni  23805  cfinfil  23813  csdfil  23814  fin1aufil  23852  rnelfmlem  23872  fmfnfmlem3  23876  txflf  23926  xmeterval  24353  reconn  24750  iimulcl  24866  isclmp  25030  iscau3  25211  rrxmvallem  25337  minveclem3  25362  pmltpc  25384  ovolfcl  25400  ismbl  25460  dyaddisj  25530  iblre  25728  plyun0  26135  logfaclbnd  27166  lgslem3  27243  lgsdir2lem5  27273  nosupinfsep  27677  sltrec  27767  madebdaylemlrcut  27848  addsproplem2  27917  addsuniflem  27948  negsproplem2  27975  negsid  27987  mulsproplem5  28063  mulsproplem6  28064  mulsproplem7  28065  mulsproplem8  28066  mulsproplem9  28067  mulsuniflem  28092  precsexlem9  28157  precsexlem10  28158  nnaddscl  28278  nnmulscl  28279  zaddscl  28322  zsoring  28336  recut  28400  0reno  28401  readdscl  28403  remulscl  28406  tgjustf  28453  ishpg  28739  usgrexmpllem  29240  nb3grpr2  29363  vtxd0nedgb  29469  wlk1walk  29619  clwlkcompbp  29762  wwlknllvtx  29826  wwlksonvtx  29835  wspthnonp  29839  wwlksn0s  29841  wwlksnndef  29885  2wlkdlem8  29913  elwwlks2s3  29931  clwwlkf1  30028  clwwlknonccat  30075  clwwlknon2x  30082  3pthdlem1  30143  upgr4cycl4dv4e  30164  frgr2wwlk1  30308  frgrreg  30373  ajfval  30788  issh  31187  chcon2i  31443  chcon3i  31445  spanuni  31523  5oalem7  31639  3oalem3  31643  pjin2i  32172  pjin3i  32173  cvnbtwn4  32268  mdslj1i  32298  mdslj2i  32299  mdslmd1i  32308  chrelat4i  32352  chirredi  32373  cdj3i  32420  rmoun  32473  difrab2  32477  eqdif  32498  inpr0  32511  iuninc  32539  fcoinvbr  32584  suppss2f  32612  fmptdF  32630  disjdsct  32676  f1od2  32694  hashxpe  32782  tosglblem  32946  mgcval  32959  pmtrprfv2  33060  elrgspnlem2  33210  ssdifidllem  33420  ssmxidllem  33437  ccfldextdgrr  33660  fldext2chn  33711  ordtconnlem1  33907  esumpfinvalf  34059  esum2dlem  34075  measiuns  34200  eulerpartlemt0  34353  eulerpartlemr  34358  eulerpartlemn  34365  ballotlem2  34473  ballotlemodife  34482  bnj887  34748  bnj976  34760  bnj1385  34815  bnj153  34863  bnj543  34876  bnj607  34899  bnj882  34909  bnj916  34916  bnj983  34934  derangenlem  35151  pconnconn  35211  fmlaomn0  35370  fmla0disjsuc  35378  fmlasucdisj  35379  elmpst  35516  xpab  35706  dftr6  35731  dffr5  35734  fundmpss  35747  elpotr  35762  brtxp  35861  brpprod  35866  brsset  35870  idsset  35871  dfon3  35873  ellimits  35891  dffun10  35895  elfuns  35896  brcart  35913  brimg  35918  brapply  35919  brcap  35921  brsuccf  35922  funpartfun  35924  dfrecs2  35931  dfrdg4  35932  altopthc  35952  altopthd  35953  altopelaltxp  35957  outsideoftr  36110  rmoeqbii  36169  reueqbii  36171  rabeqbii  36175  riotaeqbii  36179  ixpeq1i  36181  cbvixpvw2  36226  cbvprodvw2  36228  trer  36297  neibastop1  36340  neifg  36352  df3nandALT1  36380  imnand2  36383  eliminable-abelab  36851  bj-eldiag2  37158  bj-imdiridlem  37166  bj-opabco  37169  bj-xpcossxp  37170  topdifinfeq  37331  relowlssretop  37344  relowlpssretop  37345  wl-cases2-dnf  37493  poimirlem30  37637  poimirlem32  37639  ismblfin  37648  mbfposadd  37654  inixp  37715  elghomOLD  37874  keridl  38019  smprngopr  38039  sbcani  38095  inxpxrn  38374  dfcoss2  38397  cosscnv  38400  coss1cnvres  38401  coss2cnvepres  38402  1cossres  38413  dfcoels  38414  trressn  38429  br1cossinres  38431  br1cossinidres  38433  br1cossincnvepres  38434  br1cossxrnidres  38435  br1cossxrncnvepres  38436  cosscnvssid3  38460  coss0  38463  cossid  38464  trcoss  38466  eleccossin  38467  dfssr2  38483  br1cossxrncnvssrres  38492  refsymrels3  38550  refsymrel2  38551  refsymrel3  38552  elrefsymrels3  38554  dfeqvrel2  38574  dfeqvrel3  38575  redundeq1  38613  redundpbi1  38615  dfcomember3  38659  eqvreldmqs  38660  eqvreldmqs2  38661  dfeldisj3  38704  eldisjn0elb  38730  antisymrelres  38748  dfmembpart2  38755  prtlem10  38851  prter1  38865  lcvbr3  39009  isopos  39166  llnexatN  39508  snatpsubN  39737  pclclN  39878  pclfinN  39887  lhpocnel2  40006  cdlemk19w  40959  dih1dimatlem  41316  psspwb  42209  redvmptabs  42341  mzpclall  42708  mzpincl  42715  mzpindd  42727  2nn0ind  42927  dford4  43011  wopprc  43012  islmodfg  43051  ifpan123g  43441  ifpan23  43442  ifpnot23  43460  ifpdfxor  43469  ifpidg  43473  ifpid1g  43476  ifpim23g  43477  ifpim123g  43482  ifpim1g  43483  ifp1bi  43484  ifpimimb  43486  ifpororb  43487  ifpor123g  43490  ifpbibib  43492  rp-isfinite6  43500  alephiso2  43540  undmrnresiss  43586  cotrintab  43596  brtrclfv2  43709  dfxor4  43748  snhesn  43768  dffrege76  43921  uneqsn  44007  expandan  44270  ismnuprim  44276  nzin  44300  onfrALTlem5  44525  onfrALTlem4  44526  undif3VD  44864  onfrALTlem5VD  44867  onfrALTlem4VD  44868  dfac5prim  44973  wfaxpr  44981  brpermmodel  44986  permac8prim  44997  ndisj2  45038  rexabsle  45408  ellimcabssub0  45608  limsupre2mpt  45721  limsupre3  45724  limsupre3mpt  45725  limsupre3uz  45727  limsupreuz  45728  liminfreuz  45794  fourierdlem103  46200  fourierdlem104  46201  fourierdlem112  46209  smflim  46768  smflim2  46797  smflimsuplem1  46811  smflimsup  46819  cfsetsnfsetf1  47053  2reu8i  47107  ichan  47449  clnbgrsym  47831  dfnbgr6  47850  upgrimpthslem2  47901  isgrlim  47974  usgrexmpl2trifr  48021  pgnbgreunbgrlem5  48106  pgnbgreunbgr  48108  2zlidl  48221  islininds2  48466  zlmodzxzldeplem3  48484  2itscp  48763  reutruALT  48786  iinxp  48812  0funclem  49068  fucofulem2  49293  fuco2el  49294  catcinv  49381  2arwcatlem1  49577  alsi-no-surprise  49778