Theorem anbi12i 639

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anbi12ci  640  an2anr  647  ordi  1023  ordir  1024  orddi  1027  pm5.17  1029  xor  1032  cases2  1063  3anbi123i  1173  an6  1474  nanbi  1530  cadan  1639  nic-axALT  1704  19.43OLD  1913  sbbi  2342  aaan  2365  sbnf2  2390  cbveuvw  2633  cbveuw  2634  cbveuALT  2636  2mo2  2675  2eu4  2682  sbabel  2957  neanior  3051  r19.26m  3124  reeanlem  3236  rexeqbii  3337  reu5  3371  cbvreuw  3395  cgsex4g  3501  reu2  3688  reu3  3690  2reu5a  3707  2reu5lem3  3720  2reu1  3851  eqss  3952  unss  4143  ralunb  4150  ssin  4191  undi  4238  indifdi  4247  undif3  4253  inab  4262  difab  4263  reuss2  4279  reupick  4282  2reu4lem  4484  reuprg  4669  sstp  4801  tpss  4802  prneimg  4819  prneimg2  4820  prnebg  4821  uniinOLD  4897  intun  4945  disjiun  5097  disjxiun  5106  brin  5163  brdif  5164  ssext  5435  pweqb  5437  opthg2  5461  copsex4g  5478  propeqop  5490  eqopab2bw  5533  eqopab2b  5537  pwin  5552  pofun  5587  dffr6  5617  wetrep  5654  elxp3  5727  soinxp  5743  weinxp  5746  csbxp  5762  relun  5798  inopab  5816  difopab  5817  inxp  5818  opelco2g  5853  cnvco  5875  dmin  5901  restidsing  6055  intasym  6115  asymref  6116  asymref2  6117  cnvdif  6140  xpnz  6156  difxp  6161  xpdifid  6165  xpdifcnvepel  6166  xp11  6173  dfco2  6246  cnvpo  6288  cnvso  6289  xpco  6290  reu3op  6293  dfpo2  6297  dffun4  6549  funun  6582  fun11  6610  fununi  6611  imadif  6620  fnres  6662  mptfnf  6670  fnopabg  6672  fun  6740  fin  6758  dff1o2  6826  brprcneu  6871  brprcneuALT  6872  dffv2  6976  fsn  7131  f13dfv  7272  dff1o6  7273  isotr  7334  eqoprab2bw  7480  eqoprab2b  7481  fvmpopr2d  7572  porpss  7724  epweon  7770  onsucb  7809  resf1extb  7927  elxp6  8016  dfoprab3  8047  opiota  8052  poxp  8120  soxp  8121  poxp2  8135  xpord2pred  8137  xpord2indlem  8139  xpord3pred  8144  xpord3inddlem  8146  soseq  8151  suppvalbr  8156  brtpos2  8224  frrlem9  8287  fprlem1  8293  tfrlem7  8366  dfer2  8691  eqer  8727  iiner  8783  uniinqs  8791  brecop  8804  eroveu  8806  erovlem  8807  fsetexb  8857  mapval2  8866  ixpin  8917  boxriin  8934  brsdom  8967  xpcomco  9051  xpassen  9055  sbthlem9  9079  sbthlem10  9080  brsdom2  9085  ssenen  9135  sbthfilem  9178  dffi3  9387  dfsup2  9400  infcllem  9444  axinf2  9605  zfinf2  9607  oemapso  9647  ttrcltr  9681  frrlem15  9725  scottexs  9857  scott0s  9858  kardex  9876  karden  9877  dfac5lem1  10103  dfac5lem3  10105  kmlem15  10144  enfin2i  10300  fin23lem34  10325  brdom7disj  10510  fpwwe2lem11  10621  fpwwe2lem12  10622  axgroth5  10804  grothprim  10814  addsrpr  11055  mulsrpr  11056  mulgt0sr  11085  addcnsr  11115  mulcnsr  11116  ltresr  11120  axcnre  11144  ssxr  11274  infrenegsup  12193  nnwos  12934  zmin  12963  xrnemnf  13137  xrnepnf  13138  xmullem  13285  xmulcom  13287  xmulneg1  13290  xmulf  13293  xrinfmss2  13332  elfzuzb  13541  fzass4  13586  seqof  14091  hashbclem  14485  hashfacen  14487  xpcogend  15007  trclublem  15028  rexanre  15394  caubnd  15406  o1lo1  15584  rpnnen2lem12  16276  lcmcllem  16649  lcmftp  16689  lcmfunsnlem2  16693  isprm3  16736  prmreclem2  16972  4sqlem12  17011  catcone0  17738  isffth2  17970  fucinv  18028  lublecllem  18409  odulub  18456  oduglb  18458  issubmgm  18755  rabsubmgmd  18757  mndpsuppss  18818  issubm  18856  issubmd  18859  0subm  18871  insubm  18872  sursubmefmnd  18950  injsubmefmnd  18951  smndex1mgm  18964  isnsg2  19217  cycsubm  19268  oppgid  19421  symgfixf1  19502  pmtrrn2  19525  lsmdisjr  19749  lsmhash  19770  gsumcom3  20043  dprd0  20098  issrg  20265  dvdsrtr  20446  isirred2  20499  isdomn3  20813  opprdomnb  20815  isdomn4r  20817  lss1d  21084  lspsolvlem  21266  lbsextlem2  21283  ssdifidllem  21484  cnfldfun  21536  unocv  21830  iunocv  21831  evlsval  22237  mpomatmul  22603  cpmidpmat  23030  tgval2  23113  fctop  23161  ppttop  23164  epttop  23166  cnnei  23439  2ndcctbss  23612  txuni2  23722  txbas  23724  ptbasin  23734  txdis1cn  23792  xkococnlem  23816  opnfbas  23999  fgcl  24035  fbasrn  24041  filuni  24042  cfinfil  24050  csdfil  24051  fin1aufil  24089  rnelfmlem  24109  fmfnfmlem3  24113  txflf  24163  xmeterval  24589  reconn  24986  iimulcl  25096  isclmp  25256  iscau3  25437  rrxmvallem  25563  minveclem3  25588  pmltpc  25609  ovolfcl  25625  ismbl  25685  dyaddisj  25755  iblre  25953  plyun0  26354  logfaclbnd  27386  lgslem3  27463  lgsdir2lem5  27493  nosupinfsep  27896  ltsrec  27994  madebdaylemlrcut  28092  addsproplem2  28163  addsuniflem  28194  negsproplem2  28222  negsid  28234  mulsproplem5  28313  mulsproplem6  28314  mulsproplem7  28315  mulsproplem8  28316  mulsproplem9  28317  mulsuniflem  28342  precsexlem9  28408  precsexlem10  28409  ons2ind  28468  nnaddscl  28539  nnmulscl  28540  zaddscl  28587  zsoring  28602  recut  28687  readdscl  28692  remulscl  28695  tgjustf  28742  ishpg  29041  usgrexmpllem  29610  nb3grpr2  29733  vtxd0nedgb  29838  wlk1walk  29988  clwlkcompbp  30131  wwlknllvtx  30195  wwlksonvtx  30204  wspthnonp  30208  wwlksn0s  30210  wwlksnndef  30254  2wlkdlem8  30282  elwwlks2s3  30300  clwwlkf1  30400  clwwlknonccat  30447  clwwlknon2x  30454  3pthdlem1  30515  upgr4cycl4dv4e  30536  frgr2wwlk1  30680  frgrreg  30745  ajfval  31161  issh  31560  chcon2i  31816  chcon3i  31818  spanuni  31896  5oalem7  32012  3oalem3  32016  pjin2i  32545  pjin3i  32546  cvnbtwn4  32641  mdslj1i  32671  mdslj2i  32672  mdslmd1i  32681  chrelat4i  32725  chirredi  32746  cdj3i  32793  rmoun  32840  difrab2  32844  eqdif  32865  inpr0  32878  iuninc  32905  fcoinvbr  32950  suppss2f  32983  fmptdF  33001  disjdsct  33048  f1od2  33064  hashxpe  33152  tosglblem  33294  mgcval  33307  pmtrprfv2  33408  elrgspnlem2  33563  ssmxidllem  33756  ccfldextdgrr  34062  fldext2chn  34118  ordtconnlem1  34314  esumpfinvalf  34466  esum2dlem  34482  measiuns  34607  eulerpartlemt0  34759  eulerpartlemr  34764  eulerpartlemn  34771  ballotlem2  34879  ballotlemodife  34888  bnj887  35154  bnj976  35166  bnj1385  35220  bnj153  35268  bnj543  35281  bnj607  35304  bnj882  35314  bnj916  35321  bnj983  35339  axreg  35540  axregscl  35541  axregs  35552  onvfowev  35600  derangenlem  35663  pconnconn  35723  fmlaomn0  35882  fmla0disjsuc  35890  fmlasucdisj  35891  elmpst  36028  xpab  36218  dftr6  36243  dffr5  36246  fundmpss  36259  elpotr  36271  brtxp  36370  brpprod  36375  brsset  36379  idsset  36380  dfon3  36382  ellimits  36400  dffun10  36404  elfuns  36405  brcart  36422  brimg  36427  brapply  36428  brcap  36430  lemsuccf  36431  funpartfun  36435  dfrecs2  36442  dfrdg4  36443  altopthc  36463  altopthd  36464  altopelaltxp  36468  outsideoftr  36621  rmoeqbii  36720  reueqbii  36722  rabeqbii  36726  riotaeqbii  36730  ixpeq1i  36732  cbvixpvw2  36777  cbvprodvw2  36779  trer  36847  neibastop1  36890  neifg  36902  df3nandALT1  36930  imnand2  36933  axtco  37002  regsfromregtco  37069  regsfromunir1  37071  mh-prprimbi  37074  eliminable-abelab  37525  bj-eldiag2  37841  bj-imdiridlem  37849  bj-opabco  37852  bj-xpcossxp  37853  topdifinfeq  38016  relowlssretop  38029  relowlpssretop  38030  wl-cases2-dnf  38187  poimirlem30  38321  poimirlem32  38323  ismblfin  38332  mbfposadd  38338  inixp  38399  elghomOLD  38558  keridl  38703  smprngopr  38723  sbcani  38777  inxpxrn  39087  dfcoss2  39172  cosscnv  39175  coss1cnvres  39176  coss2cnvepres  39177  1cossres  39188  dfcoels  39189  trressn  39204  br1cossinres  39206  br1cossinidres  39208  br1cossincnvepres  39209  br1cossxrnidres  39210  br1cossxrncnvepres  39211  cosscnvssid3  39235  coss0  39238  cossid  39239  trcoss  39241  eleccossin  39242  dfssr2  39248  br1cossxrncnvssrres  39257  refsymrels3  39319  refsymrel2  39320  refsymrel3  39321  elrefsymrels3  39323  dfeqvrel2  39343  dfeqvrel3  39344  redundeq1  39382  redundpbi1  39384  dfcomember3  39428  eqvreldmqs  39429  eqvreldmqs2  39430  dfeldisj3  39480  eldisjdmqsim  39486  eldisjn0elb  39514  antisymrelres  39535  dfmembpart2  39542  prtlem10  39659  prter1  39673  lcvbr3  39817  isopos  39974  llnexatN  40315  snatpsubN  40544  pclclN  40685  pclfinN  40694  lhpocnel2  40813  cdlemk19w  41766  dih1dimatlem  42123  psspwb  43019  redvmptabs  43141  mzpclall  43478  mzpincl  43485  mzpindd  43497  2nn0ind  43692  dford4  43776  wopprc  43777  islmodfg  43816  ifpan123g  44205  ifpan23  44206  ifpnot23  44224  ifpdfxor  44233  ifpidg  44237  ifpid1g  44240  ifpim23g  44241  ifpim123g  44246  ifpim1g  44247  ifp1bi  44248  ifpimimb  44250  ifpororb  44251  ifpor123g  44254  ifpbibib  44256  rp-isfinite6  44264  alephiso2  44304  undmrnresiss  44350  cotrintab  44360  brtrclfv2  44473  dfxor4  44512  snhesn  44532  dffrege76  44685  uneqsn  44771  expandan  45018  ismnuprim  45024  nzin  45048  onfrALTlem5  45271  onfrALTlem4  45272  undif3VD  45610  onfrALTlem5VD  45613  onfrALTlem4VD  45614  dfac5prim  45719  wfaxpr  45727  brpermmodel  45732  permac8prim  45743  ndisj2  45791  rexabsle  46153  ellimcabssub0  46353  limsupre2mpt  46464  limsupre3  46467  limsupre3mpt  46468  limsupre3uz  46470  limsupreuz  46471  liminfreuz  46537  fourierdlem103  46943  fourierdlem104  46944  fourierdlem112  46952  smflim  47511  smflim2  47540  smflimsuplem1  47554  smflimsup  47562  cfsetsnfsetf1  47816  2reu8i  47870  ichan  48224  clnbgrsym  48623  dfnbgr6  48642  upgrimpthslem2  48693  isgrlim  48767  usgrexmpl2trifr  48822  pgnbgreunbgrlem5  48908  pgnbgreunbgr  48910  2zlidl  49025  smprngprmrng  49124  islininds2  49284  zlmodzxzldeplem3  49302  2itscp  49581  reutruALT  49603  iinxp  49629  0funclem  49884  fucofulem2  50109  fuco2el  50110  catcinv  50197  2arwcatlem1  50393  dfrals2  50588  alsbii  50598  ralsbii  50599  cbvals  50603  als-no-surprise  50604  rals-no-surprise  50605  dfralseu2  50621  alseubii  50630  ralseubii  50631