Theorem anbi12i 627

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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anbi12ci  628  an2anr  635  ordi  1004  ordir  1005  orddi  1008  pm5.17  1010  xor  1013  cases2  1046  3anbi123i  1153  an6  1442  nanbi  1494  cadan  1603  nic-axALT  1669  19.43OLD  1879  sbbi  2298  aaan  2323  sbnf2  2350  eubii  2575  cbveuvw  2596  cbveuw  2597  cbveuALT  2600  2mo2  2639  2eu4  2646  sbabel  2934  sbabelOLD  2935  neanior  3031  r19.26m  3106  reeanlem  3221  2ralorOLD  3225  rexeqbii  3335  reu5  3374  cbvreuw  3402  cgsex4g  3517  reu2  3719  reu3  3721  2reu5a  3738  2reu5lem3  3751  2reu1  3888  eqss  3994  ss2abdv  4057  unss  4181  ralunb  4188  ssin  4227  undi  4271  indifdi  4280  indifdirOLD  4282  undif3  4287  inab  4296  difab  4297  reuss2  4312  reupick  4315  2reu4lem  4522  reuprg  4704  sstp  4834  tpss  4835  prneimg  4852  prnebg  4853  uniin  4930  intun  4979  intprOLD  4982  disjiun  5130  disjxiun  5140  brin  5195  brdif  5196  ssext  5451  pweqb  5453  opthg2  5476  copsex4g  5492  propeqop  5504  eqopab2bw  5545  eqopab2b  5549  pwin  5567  pofun  5603  dffr6  5631  wetrep  5666  elxp3  5739  soinxp  5754  weinxp  5757  csbxp  5772  relun  5808  inopab  5826  difopab  5827  difopabOLD  5828  inxp  5829  inxpOLD  5830  opelco2g  5865  cnvco  5883  dmin  5909  restidsing  6051  intasym  6116  asymref  6117  asymref2  6118  cnvdif  6143  xpnz  6158  difxp  6163  xpdifid  6167  xp11  6174  dfco2  6244  relssdmrnOLD  6268  cnvpo  6286  cnvso  6287  xpco  6288  reu3op  6291  dfpo2  6295  dffun4  6559  funun  6594  fun11  6622  fununi  6623  imadif  6632  fnres  6677  mptfnf  6685  fnopabg  6687  fun  6754  fin  6772  dff1o2  6839  brprcneu  6882  brprcneuALT  6883  dffv2  6988  fsn  7139  f13dfv  7278  dff1o6  7279  isotr  7339  eqoprab2bw  7485  eqoprab2b  7486  fvmpopr2d  7578  porpss  7727  epweon  7772  onsucb  7815  elxp6  8022  dfoprab3  8053  opiota  8058  poxp  8128  soxp  8129  poxp2  8143  xpord2pred  8145  xpord2indlem  8147  xpord3pred  8152  xpord3inddlem  8154  soseq  8159  suppvalbr  8164  brtpos2  8232  frrlem9  8294  fprlem1  8300  wfrlem5OLD  8328  wfrfunOLD  8334  tfrlem7  8398  dfer2  8720  eqer  8754  iiner  8802  uniinqs  8810  brecop  8823  eroveu  8825  erovlem  8826  fsetexb  8877  mapval2  8885  ixpin  8936  boxriin  8953  brsdom  8990  xpcomco  9081  xpassen  9085  sbthlem9  9110  sbthlem10  9111  brsdom2  9116  ssenen  9170  sbthfilem  9220  unfiOLD  9332  dffi3  9449  dfsup2  9462  infcllem  9505  axinf2  9658  zfinf2  9660  oemapso  9700  ttrcltr  9734  frrlem15  9775  scottexs  9905  scott0s  9906  kardex  9912  karden  9913  dfac5lem1  10141  dfac5lem3  10143  kmlem15  10182  enfin2i  10339  fin23lem34  10364  brdom7disj  10549  fpwwe2lem11  10659  fpwwe2lem12  10660  axgroth5  10842  grothprim  10852  addsrpr  11093  mulsrpr  11094  mulgt0sr  11123  addcnsr  11153  mulcnsr  11154  ltresr  11158  axcnre  11182  1re  11239  ssxr  11308  infrenegsup  12222  nnwos  12924  zmin  12953  xrnemnf  13124  xrnepnf  13125  xmullem  13270  xmulcom  13272  xmulneg1  13275  xmulf  13278  xrinfmss2  13317  elfzuzb  13522  fzass4  13566  seqof  14051  hashbclem  14438  hashfacen  14440  hashfacenOLD  14441  xpcogend  14948  trclublem  14969  rexanre  15320  caubnd  15332  o1lo1  15508  rpnnen2lem12  16196  lcmcllem  16561  lcmftp  16601  lcmfunsnlem2  16605  isprm3  16648  prmreclem2  16880  4sqlem12  16919  catcone0  17661  isffth2  17899  fucinv  17959  lublecllem  18346  odulub  18393  oduglb  18395  issubmgm  18656  rabsubmgmd  18658  issubm  18749  issubmd  18752  0subm  18763  insubm  18764  sursubmefmnd  18842  injsubmefmnd  18843  smndex1mgm  18853  isnsg2  19105  cycsubm  19151  oppgid  19304  symgfixf1  19386  pmtrrn2  19409  lsmdisjr  19633  lsmhash  19654  gsumcom3  19927  dprd0  19982  issrg  20122  dvdsrtr  20301  isirred2  20354  lss1d  20841  lspsolvlem  21024  lbsextlem2  21041  isdomn3  21242  cnfldfun  21287  cnfldfunOLD  21300  unocv  21606  iunocv  21607  evlsval  22026  mpomatmul  22342  cpmidpmat  22769  tgval2  22853  fctop  22901  ppttop  22904  epttop  22906  cnnei  23180  2ndcctbss  23353  txuni2  23463  txbas  23465  ptbasin  23475  txdis1cn  23533  xkococnlem  23557  opnfbas  23740  fgcl  23776  fbasrn  23782  filuni  23783  cfinfil  23791  csdfil  23792  fin1aufil  23830  rnelfmlem  23850  fmfnfmlem3  23854  txflf  23904  xmeterval  24332  reconn  24738  iimulcl  24854  isclmp  25018  iscau3  25200  rrxmvallem  25326  minveclem3  25351  pmltpc  25373  ovolfcl  25389  ismbl  25449  dyaddisj  25519  iblre  25717  plyun0  26125  logfaclbnd  27149  lgslem3  27226  lgsdir2lem5  27256  nosupinfsep  27659  nocvxmin  27705  sltrec  27747  madebdaylemlrcut  27819  addsproplem2  27881  addsuniflem  27912  negsproplem2  27935  negsid  27947  mulsproplem5  28014  mulsproplem6  28015  mulsproplem7  28016  mulsproplem8  28017  mulsproplem9  28018  mulsuniflem  28043  precsexlem9  28107  precsexlem10  28108  nnaddscl  28206  nnmulscl  28207  recut  28218  0reno  28219  readdscl  28221  remulscl  28224  tgjustf  28271  ishpg  28557  usgrexmpllem  29067  nb3grpr2  29190  vtxd0nedgb  29296  wlk1walk  29447  clwlkcompbp  29590  wwlknllvtx  29651  wwlksonvtx  29660  wspthnonp  29664  wwlksn0s  29666  wwlksnndef  29710  2wlkdlem8  29738  elwwlks2s3  29756  clwwlkf1  29853  clwwlknonccat  29900  clwwlknon2x  29907  3pthdlem1  29968  upgr4cycl4dv4e  29989  frgr2wwlk1  30133  frgrreg  30198  ajfval  30613  issh  31012  chcon2i  31268  chcon3i  31270  spanuni  31348  5oalem7  31464  3oalem3  31468  pjin2i  31997  pjin3i  31998  cvnbtwn4  32093  mdslj1i  32123  mdslj2i  32124  mdslmd1i  32133  chrelat4i  32177  chirredi  32198  cdj3i  32245  rmoun  32286  difrab2  32290  eqdif  32310  inpr0  32322  iuninc  32345  fcoinvbr  32389  suppss2f  32418  fmptdF  32436  disjdsct  32477  cnvoprabOLD  32497  f1od2  32498  hashxpe  32571  tosglblem  32696  mgcval  32709  pmtrprfv2  32806  ssmxidllem  33181  ccfldextdgrr  33351  ordtconnlem1  33520  esumpfinvalf  33690  esum2dlem  33706  measiuns  33831  eulerpartlemt0  33984  eulerpartlemr  33989  eulerpartlemn  33996  ballotlem2  34103  ballotlemodife  34112  bnj887  34391  bnj976  34403  bnj1385  34458  bnj153  34506  bnj543  34519  bnj607  34542  bnj882  34552  bnj916  34559  bnj983  34577  derangenlem  34776  pconnconn  34836  fmlaomn0  34995  fmla0disjsuc  35003  fmlasucdisj  35004  elmpst  35141  xpab  35315  dftr6  35340  dffr5  35343  fundmpss  35357  elpotr  35372  brtxp  35471  brpprod  35476  brsset  35480  idsset  35481  dfon3  35483  ellimits  35501  dffun10  35505  elfuns  35506  brcart  35523  brimg  35528  brapply  35529  brcap  35531  brsuccf  35532  funpartfun  35534  dfrecs2  35541  dfrdg4  35542  altopthc  35562  altopthd  35563  altopelaltxp  35567  outsideoftr  35720  trer  35795  neibastop1  35838  neifg  35850  df3nandALT1  35878  imnand2  35881  eliminable-abelab  36342  bj-eldiag2  36651  bj-imdiridlem  36659  bj-opabco  36662  bj-xpcossxp  36663  topdifinfeq  36824  relowlssretop  36837  relowlpssretop  36838  wl-cases2-dnf  36974  poimirlem30  37118  poimirlem32  37120  ismblfin  37129  mbfposadd  37135  inixp  37196  elghomOLD  37355  keridl  37500  smprngopr  37520  sbcani  37576  inxpxrn  37862  dfcoss2  37880  cosscnv  37883  coss1cnvres  37884  coss2cnvepres  37885  1cossres  37896  dfcoels  37897  trressn  37912  br1cossinres  37914  br1cossinidres  37916  br1cossincnvepres  37917  br1cossxrnidres  37918  br1cossxrncnvepres  37919  cosscnvssid3  37943  coss0  37946  cossid  37947  trcoss  37949  eleccossin  37950  dfssr2  37966  br1cossxrncnvssrres  37975  refsymrels3  38033  refsymrel2  38034  refsymrel3  38035  elrefsymrels3  38037  dfeqvrel2  38057  dfeqvrel3  38058  redundeq1  38096  redundpbi1  38098  dfcomember3  38141  eqvreldmqs  38142  eqvreldmqs2  38143  dfeldisj3  38186  eldisjn0elb  38212  antisymrelres  38230  dfmembpart2  38237  prtlem10  38332  prter1  38346  lcvbr3  38490  isopos  38647  llnexatN  38989  snatpsubN  39218  pclclN  39359  pclfinN  39368  lhpocnel2  39487  cdlemk19w  40440  dih1dimatlem  40797  psspwb  41707  mzpclall  42138  mzpincl  42145  mzpindd  42157  2nn0ind  42357  dford4  42441  wopprc  42442  islmodfg  42484  ifpan123g  42880  ifpan23  42881  ifpnot23  42899  ifpdfxor  42908  ifpidg  42912  ifpid1g  42915  ifpim23g  42916  ifpim123g  42921  ifpim1g  42922  ifp1bi  42923  ifpimimb  42925  ifpororb  42926  ifpor123g  42929  ifpbibib  42931  rp-isfinite6  42939  alephiso2  42979  undmrnresiss  43025  cotrintab  43035  brtrclfv2  43148  dfxor4  43187  snhesn  43207  dffrege76  43360  uneqsn  43446  expandan  43716  ismnuprim  43722  nzin  43746  onfrALTlem5  43972  onfrALTlem4  43973  undif3VD  44312  onfrALTlem5VD  44315  onfrALTlem4VD  44316  ndisj2  44406  rexabsle  44792  ellimcabssub0  44996  limsupre2mpt  45109  limsupre3  45112  limsupre3mpt  45113  limsupre3uz  45115  limsupreuz  45116  liminfreuz  45182  fourierdlem103  45588  fourierdlem104  45589  fourierdlem112  45597  smflim  46156  smflim2  46185  smflimsuplem1  46199  smflimsup  46207  cfsetsnfsetf1  46432  2reu8i  46484  ichan  46786  gricer  47181  2zlidl  47293  mndpsuppss  47426  islininds2  47543  zlmodzxzldeplem3  47561  2itscp  47845  reutruALT  47868  alsi-no-surprise  48220