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  1446  nanbi  1499  cadan  1608  nic-axALT  1673  19.43OLD  1882  sbbi  2307  aaan  2331  sbnf2  2359  eubii  2583  cbveuvw  2603  cbveuw  2604  cbveuALT  2606  2mo2  2645  2eu4  2653  sbabel  2930  neanior  3024  r19.26m  3097  reeanlem  3215  2ralorOLD  3219  rexeqbii  3329  reu5  3366  cbvreuw  3394  cgsex4g  3512  reu2  3715  reu3  3717  2reu5a  3734  2reu5lem3  3747  2reu1  3879  eqss  3981  unss  4172  ralunb  4179  ssin  4221  undi  4267  indifdi  4276  undif3  4282  inab  4291  difab  4292  reuss2  4308  reupick  4311  2reu4lem  4504  reuprg  4685  sstp  4818  tpss  4819  prneimg  4836  prneimg2  4837  prnebg  4838  uniin  4913  intun  4962  disjiun  5113  disjxiun  5122  brin  5177  brdif  5178  ssext  5441  pweqb  5443  opthg2  5466  copsex4g  5482  propeqop  5494  eqopab2bw  5535  eqopab2b  5539  pwin  5556  pofun  5592  dffr6  5622  wetrep  5660  elxp3  5733  soinxp  5749  weinxp  5752  csbxp  5767  relun  5803  inopab  5821  difopab  5822  difopabOLD  5823  inxp  5824  inxpOLD  5825  opelco2g  5860  cnvco  5878  dmin  5904  restidsing  6053  intasym  6117  asymref  6118  asymref2  6119  cnvdif  6145  xpnz  6161  difxp  6166  xpdifid  6170  xp11  6177  dfco2  6247  relssdmrnOLD  6271  cnvpo  6289  cnvso  6290  xpco  6291  reu3op  6294  dfpo2  6298  dffun4  6558  funun  6593  fun11  6621  fununi  6622  imadif  6631  fnres  6676  mptfnf  6684  fnopabg  6686  fun  6751  fin  6769  dff1o2  6834  brprcneu  6877  brprcneuALT  6878  dffv2  6985  fsn  7136  f13dfv  7277  dff1o6  7278  isotr  7339  eqoprab2bw  7486  eqoprab2b  7487  fvmpopr2d  7578  porpss  7730  epweon  7778  onsucb  7820  resf1extb  7939  elxp6  8031  dfoprab3  8062  opiota  8067  poxp  8136  soxp  8137  poxp2  8151  xpord2pred  8153  xpord2indlem  8155  xpord3pred  8160  xpord3inddlem  8162  soseq  8167  suppvalbr  8172  brtpos2  8240  frrlem9  8302  fprlem1  8308  wfrlem5OLD  8336  wfrfunOLD  8342  tfrlem7  8406  dfer2  8729  eqer  8764  iiner  8812  uniinqs  8820  brecop  8833  eroveu  8835  erovlem  8836  fsetexb  8887  mapval2  8895  ixpin  8946  boxriin  8963  brsdom  8998  xpcomco  9085  xpassen  9089  sbthlem9  9114  sbthlem10  9115  brsdom2  9120  ssenen  9174  sbthfilem  9221  dffi3  9454  dfsup2  9467  infcllem  9510  axinf2  9663  zfinf2  9665  oemapso  9705  ttrcltr  9739  frrlem15  9780  scottexs  9910  scott0s  9911  kardex  9917  karden  9918  dfac5lem1  10146  dfac5lem3  10148  kmlem15  10188  enfin2i  10344  fin23lem34  10369  brdom7disj  10554  fpwwe2lem11  10664  fpwwe2lem12  10665  axgroth5  10847  grothprim  10857  addsrpr  11098  mulsrpr  11099  mulgt0sr  11128  addcnsr  11158  mulcnsr  11159  ltresr  11163  axcnre  11187  1re  11244  ssxr  11313  infrenegsup  12234  nnwos  12940  zmin  12969  xrnemnf  13142  xrnepnf  13143  xmullem  13289  xmulcom  13291  xmulneg1  13294  xmulf  13297  xrinfmss2  13336  elfzuzb  13541  fzass4  13585  seqof  14083  hashbclem  14474  hashfacen  14476  xpcogend  14996  trclublem  15017  rexanre  15368  caubnd  15380  o1lo1  15556  rpnnen2lem12  16244  lcmcllem  16616  lcmftp  16656  lcmfunsnlem2  16660  isprm3  16703  prmreclem2  16938  4sqlem12  16977  catcone0  17706  isffth2  17939  fucinv  17997  lublecllem  18379  odulub  18426  oduglb  18428  issubmgm  18689  rabsubmgmd  18691  mndpsuppss  18752  issubm  18790  issubmd  18793  0subm  18804  insubm  18805  sursubmefmnd  18883  injsubmefmnd  18884  smndex1mgm  18894  isnsg2  19148  cycsubm  19194  oppgid  19348  symgfixf1  19428  pmtrrn2  19451  lsmdisjr  19675  lsmhash  19696  gsumcom3  19969  dprd0  20024  issrg  20158  dvdsrtr  20341  isirred2  20394  isdomn3  20688  opprdomnb  20690  isdomn4r  20692  lss1d  20934  lspsolvlem  21117  lbsextlem2  21134  cnfldfun  21345  cnfldfunOLD  21358  unocv  21665  iunocv  21666  evlsval  22077  mpomatmul  22419  cpmidpmat  22846  tgval2  22929  fctop  22977  ppttop  22980  epttop  22982  cnnei  23255  2ndcctbss  23428  txuni2  23538  txbas  23540  ptbasin  23550  txdis1cn  23608  xkococnlem  23632  opnfbas  23815  fgcl  23851  fbasrn  23857  filuni  23858  cfinfil  23866  csdfil  23867  fin1aufil  23905  rnelfmlem  23925  fmfnfmlem3  23929  txflf  23979  xmeterval  24406  reconn  24805  iimulcl  24921  isclmp  25085  iscau3  25267  rrxmvallem  25393  minveclem3  25418  pmltpc  25440  ovolfcl  25456  ismbl  25516  dyaddisj  25586  iblre  25784  plyun0  26191  logfaclbnd  27221  lgslem3  27298  lgsdir2lem5  27328  nosupinfsep  27732  nocvxmin  27778  sltrec  27820  madebdaylemlrcut  27892  addsproplem2  27958  addsuniflem  27989  negsproplem2  28016  negsid  28028  mulsproplem5  28101  mulsproplem6  28102  mulsproplem7  28103  mulsproplem8  28104  mulsproplem9  28105  mulsuniflem  28130  precsexlem9  28194  precsexlem10  28195  nnaddscl  28304  nnmulscl  28305  zaddscl  28335  recut  28383  0reno  28384  readdscl  28386  remulscl  28389  tgjustf  28436  ishpg  28722  usgrexmpllem  29224  nb3grpr2  29347  vtxd0nedgb  29453  wlk1walk  29604  clwlkcompbp  29749  wwlknllvtx  29813  wwlksonvtx  29822  wspthnonp  29826  wwlksn0s  29828  wwlksnndef  29872  2wlkdlem8  29900  elwwlks2s3  29918  clwwlkf1  30015  clwwlknonccat  30062  clwwlknon2x  30069  3pthdlem1  30130  upgr4cycl4dv4e  30151  frgr2wwlk1  30295  frgrreg  30360  ajfval  30775  issh  31174  chcon2i  31430  chcon3i  31432  spanuni  31510  5oalem7  31626  3oalem3  31630  pjin2i  32159  pjin3i  32160  cvnbtwn4  32255  mdslj1i  32285  mdslj2i  32286  mdslmd1i  32295  chrelat4i  32339  chirredi  32360  cdj3i  32407  rmoun  32460  difrab2  32464  eqdif  32485  inpr0  32497  iuninc  32520  fcoinvbr  32565  suppss2f  32595  fmptdF  32613  disjdsct  32659  f1od2  32679  hashxpe  32758  tosglblem  32910  mgcval  32923  pmtrprfv2  33054  elrgspnlem2  33193  ssdifidllem  33425  ssmxidllem  33442  ccfldextdgrr  33663  fldext2chn  33710  ordtconnlem1  33864  esumpfinvalf  34018  esum2dlem  34034  measiuns  34159  eulerpartlemt0  34312  eulerpartlemr  34317  eulerpartlemn  34324  ballotlem2  34432  ballotlemodife  34441  bnj887  34720  bnj976  34732  bnj1385  34787  bnj153  34835  bnj543  34848  bnj607  34871  bnj882  34881  bnj916  34888  bnj983  34906  derangenlem  35117  pconnconn  35177  fmlaomn0  35336  fmla0disjsuc  35344  fmlasucdisj  35345  elmpst  35482  xpab  35667  dftr6  35692  dffr5  35695  fundmpss  35708  elpotr  35723  brtxp  35822  brpprod  35827  brsset  35831  idsset  35832  dfon3  35834  ellimits  35852  dffun10  35856  elfuns  35857  brcart  35874  brimg  35879  brapply  35880  brcap  35882  brsuccf  35883  funpartfun  35885  dfrecs2  35892  dfrdg4  35893  altopthc  35913  altopthd  35914  altopelaltxp  35918  outsideoftr  36071  rmoeqbii  36130  reueqbii  36132  rabeqbii  36136  riotaeqbii  36140  ixpeq1i  36142  cbvixpvw2  36187  cbvprodvw2  36189  trer  36258  neibastop1  36301  neifg  36313  df3nandALT1  36341  imnand2  36344  eliminable-abelab  36812  bj-eldiag2  37119  bj-imdiridlem  37127  bj-opabco  37130  bj-xpcossxp  37131  topdifinfeq  37292  relowlssretop  37305  relowlpssretop  37306  wl-cases2-dnf  37454  poimirlem30  37598  poimirlem32  37600  ismblfin  37609  mbfposadd  37615  inixp  37676  elghomOLD  37835  keridl  37980  smprngopr  38000  sbcani  38056  inxpxrn  38337  dfcoss2  38355  cosscnv  38358  coss1cnvres  38359  coss2cnvepres  38360  1cossres  38371  dfcoels  38372  trressn  38387  br1cossinres  38389  br1cossinidres  38391  br1cossincnvepres  38392  br1cossxrnidres  38393  br1cossxrncnvepres  38394  cosscnvssid3  38418  coss0  38421  cossid  38422  trcoss  38424  eleccossin  38425  dfssr2  38441  br1cossxrncnvssrres  38450  refsymrels3  38508  refsymrel2  38509  refsymrel3  38510  elrefsymrels3  38512  dfeqvrel2  38532  dfeqvrel3  38533  redundeq1  38571  redundpbi1  38573  dfcomember3  38616  eqvreldmqs  38617  eqvreldmqs2  38618  dfeldisj3  38661  eldisjn0elb  38687  antisymrelres  38705  dfmembpart2  38712  prtlem10  38807  prter1  38821  lcvbr3  38965  isopos  39122  llnexatN  39464  snatpsubN  39693  pclclN  39834  pclfinN  39843  lhpocnel2  39962  cdlemk19w  40915  dih1dimatlem  41272  psspwb  42208  redvmptabs  42335  mzpclall  42683  mzpincl  42690  mzpindd  42702  2nn0ind  42902  dford4  42986  wopprc  42987  islmodfg  43026  ifpan123g  43417  ifpan23  43418  ifpnot23  43436  ifpdfxor  43445  ifpidg  43449  ifpid1g  43452  ifpim23g  43453  ifpim123g  43458  ifpim1g  43459  ifp1bi  43460  ifpimimb  43462  ifpororb  43463  ifpor123g  43466  ifpbibib  43468  rp-isfinite6  43476  alephiso2  43516  undmrnresiss  43562  cotrintab  43572  brtrclfv2  43685  dfxor4  43724  snhesn  43744  dffrege76  43897  uneqsn  43983  expandan  44252  ismnuprim  44258  nzin  44282  onfrALTlem5  44507  onfrALTlem4  44508  undif3VD  44847  onfrALTlem5VD  44850  onfrALTlem4VD  44851  dfac5prim  44952  wfaxpr  44960  ndisj2  45001  rexabsle  45375  ellimcabssub0  45577  limsupre2mpt  45690  limsupre3  45693  limsupre3mpt  45694  limsupre3uz  45696  limsupreuz  45697  liminfreuz  45763  fourierdlem103  46169  fourierdlem104  46170  fourierdlem112  46178  smflim  46737  smflim2  46766  smflimsuplem1  46780  smflimsup  46788  cfsetsnfsetf1  47017  2reu8i  47071  ichan  47388  clnbgrsym  47770  dfnbgr6  47789  isgrlim  47895  usgrexmpl2trifr  47942  2zlidl  48102  islininds2  48347  zlmodzxzldeplem3  48365  2itscp  48648  reutruALT  48671  0funclem  48876  fucofulem2  48970  fuco2el  48971  alsi-no-surprise  49311