Theorem anbi12i 637

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anbi12ci  638  an2anr  645  ordi  1019  ordir  1020  orddi  1023  pm5.17  1025  xor  1028  cases2  1059  3anbi123i  1168  an6  1466  nanbi  1520  cadan  1629  nic-axALT  1694  19.43OLD  1903  sbbi  2341  aaan  2364  sbnf2  2389  cbveuvw  2632  cbveuw  2633  cbveuALT  2635  2mo2  2674  2eu4  2681  sbabel  2956  neanior  3050  r19.26m  3121  reeanlem  3233  rexeqbii  3335  reu5  3369  cbvreuw  3393  cgsex4g  3500  reu2  3688  reu3  3690  2reu5a  3707  2reu5lem3  3720  2reu1  3850  eqss  3951  unss  4142  ralunb  4149  ssin  4190  undi  4237  indifdi  4246  undif3  4252  inab  4261  difab  4262  reuss2  4278  reupick  4281  2reu4lem  4477  reuprg  4662  sstp  4794  tpss  4795  prneimg  4812  prneimg2  4813  prnebg  4814  uniinOLD  4890  intun  4938  disjiun  5088  disjxiun  5097  brin  5152  brdif  5153  ssext  5421  pweqb  5423  opthg2  5447  copsex4g  5464  propeqop  5476  eqopab2bw  5519  eqopab2b  5523  pwin  5538  pofun  5573  dffr6  5603  wetrep  5640  elxp3  5713  soinxp  5729  weinxp  5732  csbxp  5748  relun  5784  inopab  5802  difopab  5803  inxp  5804  opelco2g  5839  cnvco  5861  dmin  5887  restidsing  6042  intasym  6102  asymref  6103  asymref2  6104  cnvdif  6127  xpnz  6144  difxp  6149  xpdifid  6153  xpdifcnvepel  6154  xp11  6161  dfco2  6232  cnvpo  6274  cnvso  6275  xpco  6276  reu3op  6279  dfpo2  6283  dffun4  6534  funun  6567  fun11  6595  fununi  6596  imadif  6605  fnres  6648  mptfnf  6656  fnopabg  6658  fun  6726  fin  6744  dff1o2  6812  brprcneu  6857  brprcneuALT  6858  dffv2  6962  fsn  7117  f13dfv  7258  dff1o6  7259  isotr  7320  eqoprab2bw  7466  eqoprab2b  7467  fvmpopr2d  7558  porpss  7710  epweon  7758  onsucb  7797  resf1extb  7915  elxp6  8004  dfoprab3  8035  opiota  8040  poxp  8108  soxp  8109  poxp2  8123  xpord2pred  8125  xpord2indlem  8127  xpord3pred  8132  xpord3inddlem  8134  soseq  8139  suppvalbr  8144  brtpos2  8212  frrlem9  8275  fprlem1  8281  tfrlem7  8354  dfer2  8679  eqer  8715  iiner  8771  uniinqs  8779  brecop  8792  eroveu  8794  erovlem  8795  fsetexb  8845  mapval2  8854  ixpin  8905  boxriin  8922  brsdom  8955  xpcomco  9039  xpassen  9043  sbthlem9  9067  sbthlem10  9068  brsdom2  9073  ssenen  9123  sbthfilem  9166  dffi3  9377  dfsup2  9390  infcllem  9434  axinf2  9595  zfinf2  9597  oemapso  9637  ttrcltr  9671  frrlem15  9715  scottexs  9845  scott0s  9846  kardex  9852  karden  9853  dfac5lem1  10079  dfac5lem3  10081  kmlem15  10121  enfin2i  10278  fin23lem34  10303  brdom7disj  10488  fpwwe2lem11  10599  fpwwe2lem12  10600  axgroth5  10782  grothprim  10792  addsrpr  11033  mulsrpr  11034  mulgt0sr  11063  addcnsr  11093  mulcnsr  11094  ltresr  11098  axcnre  11122  ssxr  11252  infrenegsup  12175  nnwos  12916  zmin  12945  xrnemnf  13119  xrnepnf  13120  xmullem  13267  xmulcom  13269  xmulneg1  13272  xmulf  13275  xrinfmss2  13314  elfzuzb  13523  fzass4  13567  seqof  14072  hashbclem  14465  hashfacen  14467  xpcogend  14987  trclublem  15008  rexanre  15374  caubnd  15386  o1lo1  15564  rpnnen2lem12  16257  lcmcllem  16630  lcmftp  16670  lcmfunsnlem2  16674  isprm3  16717  prmreclem2  16953  4sqlem12  16992  catcone0  17719  isffth2  17951  fucinv  18009  lublecllem  18390  odulub  18437  oduglb  18439  issubmgm  18736  rabsubmgmd  18738  mndpsuppss  18799  issubm  18837  issubmd  18840  0subm  18851  insubm  18852  sursubmefmnd  18930  injsubmefmnd  18931  smndex1mgm  18944  isnsg2  19197  cycsubm  19243  oppgid  19396  symgfixf1  19477  pmtrrn2  19500  lsmdisjr  19724  lsmhash  19745  gsumcom3  20018  dprd0  20073  issrg  20238  dvdsrtr  20417  isirred2  20470  isdomn3  20765  opprdomnb  20767  isdomn4r  20769  lss1d  21030  lspsolvlem  21212  lbsextlem2  21229  cnfldfun  21438  unocv  21732  iunocv  21733  evlsval  22139  mpomatmul  22506  cpmidpmat  22933  tgval2  23016  fctop  23064  ppttop  23067  epttop  23069  cnnei  23342  2ndcctbss  23515  txuni2  23625  txbas  23627  ptbasin  23637  txdis1cn  23695  xkococnlem  23719  opnfbas  23902  fgcl  23938  fbasrn  23944  filuni  23945  cfinfil  23953  csdfil  23954  fin1aufil  23992  rnelfmlem  24012  fmfnfmlem3  24016  txflf  24066  xmeterval  24492  reconn  24889  iimulcl  24999  isclmp  25159  iscau3  25340  rrxmvallem  25466  minveclem3  25491  pmltpc  25512  ovolfcl  25528  ismbl  25588  dyaddisj  25658  iblre  25856  plyun0  26257  logfaclbnd  27286  lgslem3  27363  lgsdir2lem5  27393  nosupinfsep  27796  ltsrec  27894  madebdaylemlrcut  27992  addsproplem2  28063  addsuniflem  28094  negsproplem2  28122  negsid  28134  mulsproplem5  28213  mulsproplem6  28214  mulsproplem7  28215  mulsproplem8  28216  mulsproplem9  28217  mulsuniflem  28242  precsexlem9  28308  precsexlem10  28309  ons2ind  28368  nnaddscl  28439  nnmulscl  28440  zaddscl  28487  zsoring  28502  recut  28587  readdscl  28592  remulscl  28595  tgjustf  28642  ishpg  28932  usgrexmpllem  29461  nb3grpr2  29584  vtxd0nedgb  29689  wlk1walk  29839  clwlkcompbp  29982  wwlknllvtx  30046  wwlksonvtx  30055  wspthnonp  30059  wwlksn0s  30061  wwlksnndef  30105  2wlkdlem8  30133  elwwlks2s3  30151  clwwlkf1  30251  clwwlknonccat  30298  clwwlknon2x  30305  3pthdlem1  30366  upgr4cycl4dv4e  30387  frgr2wwlk1  30531  frgrreg  30596  ajfval  31012  issh  31411  chcon2i  31667  chcon3i  31669  spanuni  31747  5oalem7  31863  3oalem3  31867  pjin2i  32396  pjin3i  32397  cvnbtwn4  32492  mdslj1i  32522  mdslj2i  32523  mdslmd1i  32532  chrelat4i  32576  chirredi  32597  cdj3i  32644  rmoun  32693  difrab2  32697  eqdif  32718  inpr0  32731  iuninc  32760  fcoinvbr  32805  suppss2f  32840  fmptdF  32858  disjdsct  32905  f1od2  32921  hashxpe  33009  tosglblem  33152  mgcval  33165  pmtrprfv2  33268  elrgspnlem2  33424  ssdifidllem  33643  ssmxidllem  33661  ccfldextdgrr  33969  fldext2chn  34025  ordtconnlem1  34221  esumpfinvalf  34373  esum2dlem  34389  measiuns  34514  eulerpartlemt0  34666  eulerpartlemr  34671  eulerpartlemn  34678  ballotlem2  34786  ballotlemodife  34795  bnj887  35061  bnj976  35073  bnj1385  35127  bnj153  35175  bnj543  35188  bnj607  35211  bnj882  35221  bnj916  35228  bnj983  35246  axreg  35423  axregscl  35424  axregs  35435  onvfowev  35459  derangenlem  35521  pconnconn  35581  fmlaomn0  35740  fmla0disjsuc  35748  fmlasucdisj  35749  elmpst  35886  xpab  36076  dftr6  36101  dffr5  36104  fundmpss  36117  elpotr  36129  brtxp  36228  brpprod  36233  brsset  36237  idsset  36238  dfon3  36240  ellimits  36258  dffun10  36262  elfuns  36263  brcart  36280  brimg  36285  brapply  36286  brcap  36288  lemsuccf  36289  funpartfun  36293  dfrecs2  36300  dfrdg4  36301  altopthc  36321  altopthd  36322  altopelaltxp  36326  outsideoftr  36479  rmoeqbii  36548  reueqbii  36550  rabeqbii  36554  riotaeqbii  36558  ixpeq1i  36560  cbvixpvw2  36605  cbvprodvw2  36607  trer  36676  neibastop1  36719  neifg  36731  df3nandALT1  36759  imnand2  36762  axtco  36831  regsfromregtco  36898  regsfromunir1  36900  mh-prprimbi  36903  eliminable-abelab  37355  bj-eldiag2  37669  bj-imdiridlem  37677  bj-opabco  37680  bj-xpcossxp  37681  topdifinfeq  37844  relowlssretop  37857  relowlpssretop  37858  wl-cases2-dnf  38015  poimirlem30  38149  poimirlem32  38151  ismblfin  38160  mbfposadd  38166  inixp  38227  elghomOLD  38386  keridl  38531  smprngopr  38551  sbcani  38607  inxpxrn  38917  dfcoss2  39002  cosscnv  39005  coss1cnvres  39006  coss2cnvepres  39007  1cossres  39018  dfcoels  39019  trressn  39034  br1cossinres  39036  br1cossinidres  39038  br1cossincnvepres  39039  br1cossxrnidres  39040  br1cossxrncnvepres  39041  cosscnvssid3  39065  coss0  39068  cossid  39069  trcoss  39071  eleccossin  39072  dfssr2  39078  br1cossxrncnvssrres  39087  refsymrels3  39149  refsymrel2  39150  refsymrel3  39151  elrefsymrels3  39153  dfeqvrel2  39173  dfeqvrel3  39174  redundeq1  39212  redundpbi1  39214  dfcomember3  39258  eqvreldmqs  39259  eqvreldmqs2  39260  dfeldisj3  39310  eldisjdmqsim  39316  eldisjn0elb  39344  antisymrelres  39365  dfmembpart2  39372  prtlem10  39489  prter1  39503  lcvbr3  39647  isopos  39804  llnexatN  40145  snatpsubN  40374  pclclN  40515  pclfinN  40524  lhpocnel2  40643  cdlemk19w  41596  dih1dimatlem  41953  psspwb  42847  redvmptabs  42969  mzpclall  43308  mzpincl  43315  mzpindd  43327  2nn0ind  43522  dford4  43606  wopprc  43607  islmodfg  43646  ifpan123g  44035  ifpan23  44036  ifpnot23  44054  ifpdfxor  44063  ifpidg  44067  ifpid1g  44070  ifpim23g  44071  ifpim123g  44076  ifpim1g  44077  ifp1bi  44078  ifpimimb  44080  ifpororb  44081  ifpor123g  44084  ifpbibib  44086  rp-isfinite6  44094  alephiso2  44134  undmrnresiss  44180  cotrintab  44190  brtrclfv2  44303  dfxor4  44342  snhesn  44362  dffrege76  44515  uneqsn  44601  expandan  44864  ismnuprim  44870  nzin  44894  onfrALTlem5  45118  onfrALTlem4  45119  undif3VD  45457  onfrALTlem5VD  45460  onfrALTlem4VD  45461  dfac5prim  45566  wfaxpr  45574  brpermmodel  45579  permac8prim  45590  ndisj2  45631  rexabsle  45993  ellimcabssub0  46193  limsupre2mpt  46304  limsupre3  46307  limsupre3mpt  46308  limsupre3uz  46310  limsupreuz  46311  liminfreuz  46377  fourierdlem103  46783  fourierdlem104  46784  fourierdlem112  46792  smflim  47351  smflim2  47380  smflimsuplem1  47394  smflimsup  47402  cfsetsnfsetf1  47653  2reu8i  47707  ichan  48061  clnbgrsym  48460  dfnbgr6  48479  upgrimpthslem2  48530  isgrlim  48604  usgrexmpl2trifr  48659  pgnbgreunbgrlem5  48745  pgnbgreunbgr  48747  2zlidl  48862  islininds2  49106  zlmodzxzldeplem3  49124  2itscp  49403  reutruALT  49426  iinxp  49452  0funclem  49707  fucofulem2  49932  fuco2el  49933  catcinv  50020  2arwcatlem1  50216  alsi-no-surprise  50417