Theorem anbi12i 634

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anbi12ci  635  an2anr  642  ordi  1013  ordir  1014  orddi  1017  pm5.17  1019  xor  1022  cases2  1053  3anbi123i  1161  an6  1453  nanbi  1507  cadan  1616  nic-axALT  1681  19.43OLD  1890  sbbi  2318  aaan  2341  sbnf2  2366  cbveuvw  2609  cbveuw  2610  cbveuALT  2612  2mo2  2651  2eu4  2658  sbabel  2933  neanior  3027  r19.26m  3098  reeanlem  3210  rexeqbii  3312  reu5  3346  cbvreuw  3370  cgsex4g  3477  reu2  3666  reu3  3668  2reu5a  3685  2reu5lem3  3698  2reu1  3829  eqss  3930  unss  4119  ralunb  4126  ssin  4167  undi  4213  indifdi  4222  undif3  4228  inab  4237  difab  4238  reuss2  4254  reupick  4257  2reu4lem  4451  reuprg  4635  sstp  4767  tpss  4768  prneimg  4785  prneimg2  4786  prnebg  4787  uniin  4862  intun  4910  disjiun  5060  disjxiun  5069  brin  5124  brdif  5125  ssext  5393  pweqb  5395  opthg2  5419  copsex4g  5436  propeqop  5448  eqopab2bw  5490  eqopab2b  5494  pwin  5509  pofun  5544  dffr6  5574  wetrep  5611  elxp3  5684  soinxp  5700  weinxp  5703  csbxp  5719  relun  5754  inopab  5772  difopab  5773  inxp  5774  opelco2g  5809  cnvco  5827  dmin  5853  restidsing  6005  intasym  6065  asymref  6066  asymref2  6067  cnvdif  6094  xpnz  6110  difxp  6115  xpdifid  6119  xp11  6126  dfco2  6196  cnvpo  6238  cnvso  6239  xpco  6240  reu3op  6243  dfpo2  6247  dffun4  6498  funun  6531  fun11  6559  fununi  6560  imadif  6569  fnres  6612  mptfnf  6620  fnopabg  6622  fun  6689  fin  6707  dff1o2  6772  brprcneu  6817  brprcneuALT  6818  dffv2  6922  fsn  7077  f13dfv  7218  dff1o6  7219  isotr  7280  eqoprab2bw  7426  eqoprab2b  7427  fvmpopr2d  7518  porpss  7670  epweon  7718  onsucb  7757  resf1extb  7874  elxp6  7965  dfoprab3  7996  opiota  8001  poxp  8068  soxp  8069  poxp2  8083  xpord2pred  8085  xpord2indlem  8087  xpord3pred  8092  xpord3inddlem  8094  soseq  8099  suppvalbr  8104  brtpos2  8172  frrlem9  8234  fprlem1  8240  tfrlem7  8312  dfer2  8634  eqer  8670  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  9552  zfinf2  9554  oemapso  9594  ttrcltr  9628  frrlem15  9672  scottexs  9802  scott0s  9803  kardex  9809  karden  9810  dfac5lem1  10036  dfac5lem3  10038  kmlem15  10078  enfin2i  10234  fin23lem34  10259  brdom7disj  10444  fpwwe2lem11  10555  fpwwe2lem12  10556  axgroth5  10738  grothprim  10748  addsrpr  10989  mulsrpr  10990  mulgt0sr  11019  addcnsr  11049  mulcnsr  11050  ltresr  11054  axcnre  11078  ssxr  11206  infrenegsup  12130  nnwos  12856  zmin  12885  xrnemnf  13059  xrnepnf  13060  xmullem  13207  xmulcom  13209  xmulneg1  13212  xmulf  13215  xrinfmss2  13254  elfzuzb  13463  fzass4  13507  seqof  14012  hashbclem  14405  hashfacen  14407  xpcogend  14927  trclublem  14948  rexanre  15300  caubnd  15312  o1lo1  15490  rpnnen2lem12  16183  lcmcllem  16556  lcmftp  16596  lcmfunsnlem2  16600  isprm3  16643  prmreclem2  16879  4sqlem12  16918  catcone0  17644  isffth2  17876  fucinv  17934  lublecllem  18315  odulub  18362  oduglb  18364  issubmgm  18661  rabsubmgmd  18663  mndpsuppss  18724  issubm  18762  issubmd  18765  0subm  18776  insubm  18777  sursubmefmnd  18855  injsubmefmnd  18856  smndex1mgm  18869  isnsg2  19122  cycsubm  19168  oppgid  19322  symgfixf1  19403  pmtrrn2  19426  lsmdisjr  19650  lsmhash  19671  gsumcom3  19944  dprd0  19999  issrg  20160  dvdsrtr  20339  isirred2  20392  isdomn3  20687  opprdomnb  20689  isdomn4r  20691  lss1d  20953  lspsolvlem  21135  lbsextlem2  21152  cnfldfun  21361  unocv  21655  iunocv  21656  evlsval  22062  mpomatmul  22429  cpmidpmat  22856  tgval2  22939  fctop  22987  ppttop  22990  epttop  22992  cnnei  23265  2ndcctbss  23438  txuni2  23548  txbas  23550  ptbasin  23560  txdis1cn  23618  xkococnlem  23642  opnfbas  23825  fgcl  23861  fbasrn  23867  filuni  23868  cfinfil  23876  csdfil  23877  fin1aufil  23915  rnelfmlem  23935  fmfnfmlem3  23939  txflf  23989  xmeterval  24415  reconn  24812  iimulcl  24922  isclmp  25082  iscau3  25263  rrxmvallem  25389  minveclem3  25414  pmltpc  25435  ovolfcl  25451  ismbl  25511  dyaddisj  25581  iblre  25779  plyun0  26180  logfaclbnd  27203  lgslem3  27280  lgsdir2lem5  27310  nosupinfsep  27714  ltsrec  27811  madebdaylemlrcut  27909  addsproplem2  27980  addsuniflem  28011  negsproplem2  28039  negsid  28051  mulsproplem5  28130  mulsproplem6  28131  mulsproplem7  28132  mulsproplem8  28133  mulsproplem9  28134  mulsuniflem  28159  precsexlem9  28225  precsexlem10  28226  ons2ind  28285  nnaddscl  28356  nnmulscl  28357  zaddscl  28404  zsoring  28419  recut  28504  readdscl  28509  remulscl  28512  tgjustf  28559  ishpg  28845  usgrexmpllem  29347  nb3grpr2  29470  vtxd0nedgb  29575  wlk1walk  29725  clwlkcompbp  29868  wwlknllvtx  29932  wwlksonvtx  29941  wspthnonp  29945  wwlksn0s  29947  wwlksnndef  29991  2wlkdlem8  30019  elwwlks2s3  30037  clwwlkf1  30137  clwwlknonccat  30184  clwwlknon2x  30191  3pthdlem1  30252  upgr4cycl4dv4e  30273  frgr2wwlk1  30417  frgrreg  30482  ajfval  30898  issh  31297  chcon2i  31553  chcon3i  31555  spanuni  31633  5oalem7  31749  3oalem3  31753  pjin2i  32282  pjin3i  32283  cvnbtwn4  32378  mdslj1i  32408  mdslj2i  32409  mdslmd1i  32418  chrelat4i  32462  chirredi  32483  cdj3i  32530  rmoun  32581  difrab2  32585  eqdif  32607  inpr0  32620  iuninc  32649  fcoinvbr  32694  suppss2f  32730  fmptdF  32748  disjdsct  32795  f1od2  32811  hashxpe  32899  tosglblem  33053  mgcval  33066  pmtrprfv2  33169  elrgspnlem2  33324  ssdifidllem  33539  ssmxidllem  33556  ccfldextdgrr  33856  fldext2chn  33912  ordtconnlem1  34108  esumpfinvalf  34260  esum2dlem  34276  measiuns  34401  eulerpartlemt0  34553  eulerpartlemr  34558  eulerpartlemn  34565  ballotlem2  34673  ballotlemodife  34682  bnj887  34948  bnj976  34960  bnj1385  35014  bnj153  35062  bnj543  35075  bnj607  35098  bnj882  35108  bnj916  35115  bnj983  35133  axreg  35308  axregscl  35309  axregs  35320  derangenlem  35399  pconnconn  35459  fmlaomn0  35618  fmla0disjsuc  35626  fmlasucdisj  35627  elmpst  35764  xpab  35954  dftr6  35979  dffr5  35982  fundmpss  35995  elpotr  36007  brtxp  36106  brpprod  36111  brsset  36115  idsset  36116  dfon3  36118  ellimits  36136  dffun10  36140  elfuns  36141  brcart  36158  brimg  36163  brapply  36164  brcap  36166  lemsuccf  36167  funpartfun  36171  dfrecs2  36178  dfrdg4  36179  altopthc  36199  altopthd  36200  altopelaltxp  36204  outsideoftr  36357  rmoeqbii  36416  reueqbii  36418  rabeqbii  36422  riotaeqbii  36426  ixpeq1i  36428  cbvixpvw2  36473  cbvprodvw2  36475  trer  36544  neibastop1  36587  neifg  36599  df3nandALT1  36627  imnand2  36630  axtco  36699  regsfromregtco  36766  regsfromunir1  36768  mh-prprimbi  36771  eliminable-abelab  37223  bj-eldiag2  37537  bj-imdiridlem  37545  bj-opabco  37548  bj-xpcossxp  37549  topdifinfeq  37712  relowlssretop  37725  relowlpssretop  37726  wl-cases2-dnf  37883  poimirlem30  38017  poimirlem32  38019  ismblfin  38028  mbfposadd  38034  inixp  38095  elghomOLD  38254  keridl  38399  smprngopr  38419  sbcani  38475  inxpxrn  38785  dfcoss2  38870  cosscnv  38873  coss1cnvres  38874  coss2cnvepres  38875  1cossres  38886  dfcoels  38887  trressn  38902  br1cossinres  38904  br1cossinidres  38906  br1cossincnvepres  38907  br1cossxrnidres  38908  br1cossxrncnvepres  38909  cosscnvssid3  38933  coss0  38936  cossid  38937  trcoss  38939  eleccossin  38940  dfssr2  38946  br1cossxrncnvssrres  38955  refsymrels3  39017  refsymrel2  39018  refsymrel3  39019  elrefsymrels3  39021  dfeqvrel2  39041  dfeqvrel3  39042  redundeq1  39080  redundpbi1  39082  dfcomember3  39126  eqvreldmqs  39127  eqvreldmqs2  39128  dfeldisj3  39178  eldisjdmqsim  39184  eldisjn0elb  39212  antisymrelres  39233  dfmembpart2  39240  prtlem10  39357  prter1  39371  lcvbr3  39515  isopos  39672  llnexatN  40013  snatpsubN  40242  pclclN  40383  pclfinN  40392  lhpocnel2  40511  cdlemk19w  41464  dih1dimatlem  41821  psspwb  42715  redvmptabs  42837  mzpclall  43176  mzpincl  43183  mzpindd  43195  2nn0ind  43390  dford4  43474  wopprc  43475  islmodfg  43514  ifpan123g  43903  ifpan23  43904  ifpnot23  43922  ifpdfxor  43931  ifpidg  43935  ifpid1g  43938  ifpim23g  43939  ifpim123g  43944  ifpim1g  43945  ifp1bi  43946  ifpimimb  43948  ifpororb  43949  ifpor123g  43952  ifpbibib  43954  rp-isfinite6  43962  alephiso2  44002  undmrnresiss  44048  cotrintab  44058  brtrclfv2  44171  dfxor4  44210  snhesn  44230  dffrege76  44383  uneqsn  44469  expandan  44732  ismnuprim  44738  nzin  44762  onfrALTlem5  44986  onfrALTlem4  44987  undif3VD  45325  onfrALTlem5VD  45328  onfrALTlem4VD  45329  dfac5prim  45434  wfaxpr  45442  brpermmodel  45447  permac8prim  45458  ndisj2  45499  rexabsle  45862  ellimcabssub0  46062  limsupre2mpt  46173  limsupre3  46176  limsupre3mpt  46177  limsupre3uz  46179  limsupreuz  46180  liminfreuz  46246  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  smflim  47220  smflim2  47249  smflimsuplem1  47263  smflimsup  47271  cfsetsnfsetf1  47522  2reu8i  47576  ichan  47930  clnbgrsym  48329  dfnbgr6  48348  upgrimpthslem2  48399  isgrlim  48473  usgrexmpl2trifr  48528  pgnbgreunbgrlem5  48614  pgnbgreunbgr  48616  2zlidl  48731  islininds2  48975  zlmodzxzldeplem3  48993  2itscp  49272  reutruALT  49295  iinxp  49321  0funclem  49576  fucofulem2  49801  fuco2el  49802  catcinv  49889  2arwcatlem1  50085  alsi-no-surprise  50286