Theorem anbi12i 629

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.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	anbi1i 626	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	3	anbi2i 625	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
5	2, 4	bitri 278	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

Syntax hints:   ↔ wb 209   ∧ 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 210  df-an 400

This theorem is referenced by:  anbi12ci  630  ordi  1003  ordir  1004  orddi  1007  pm5.17  1009  xor  1012  cases2  1043  3anbi123i  1152  an6  1442  nanbi  1491  cadan  1611  nic-axALT  1676  19.43OLD  1884  sbbi  2313  sbbivOLD  2320  sbnf2  2366  sbbiALT  2587  eubii  2645  cbveuw  2666  cbveuALT  2669  2mo2  2709  2eu4  2716  sbabel  2986  neanior  3079  r19.26m  3140  rexeqbii  3285  reeanlem  3318  2ralor  3322  reu5  3375  reu2  3664  reu3  3666  2reu5a  3683  2reu5lem3  3696  2reu1  3826  eqss  3930  ss2abdv  3991  unss  4111  ralunb  4118  ssin  4157  undi  4201  indifdir  4210  undif3  4215  inab  4223  difab  4224  reuss2  4235  reupick  4239  2reu4lem  4423  reuprg  4599  sstp  4727  tpss  4728  prneimg  4745  prnebg  4746  uniin  4824  intun  4870  intpr  4871  disjiun  5017  disjxiun  5027  brin  5082  brdif  5083  ssext  5312  pweqb  5314  opthg2  5336  copsex4g  5350  propeqop  5362  eqopab2bw  5400  eqopab2b  5404  pwin  5419  pofun  5455  wetrep  5512  elxp3  5582  soinxp  5597  weinxp  5600  csbxp  5614  relun  5648  inopab  5665  difopab  5666  inxp  5667  opelco2g  5702  cnvco  5720  dmin  5744  restidsing  5889  intasym  5942  asymref  5943  asymref2  5944  cnvdif  5969  xpnz  5983  difxp  5988  xpdifid  5992  xp11  5999  dfco2  6065  relssdmrn  6088  cnvpo  6106  cnvso  6107  xpco  6108  reu3op  6111  dffun4  6336  funun  6370  fun11  6398  fununi  6399  imadif  6408  fnres  6446  mptfnf  6455  fnopabg  6457  fun  6514  fin  6533  dff1o2  6595  brprcneu  6637  dffv2  6733  fsn  6874  f13dfv  7009  dff1o6  7010  isotr  7068  eqoprab2bw  7203  eqoprab2b  7204  fvmpopr2d  7290  porpss  7433  sucelon  7512  elxp6  7705  dfoprab3  7734  opiota  7739  poxp  7805  soxp  7806  suppvalbr  7817  brtpos2  7881  wfrlem5  7942  wfrfun  7948  tfrlem7  8002  dfer2  8273  eqer  8307  iiner  8352  uniinqs  8360  brecop  8373  eroveu  8375  erovlem  8376  mapval2  8419  ixpin  8470  boxriin  8487  brsdom  8515  xpcomco  8590  xpassen  8594  sbthlem9  8619  sbthlem10  8620  brsdom2  8625  ssenen  8675  unfi  8769  dffi3  8879  dfsup2  8892  infcllem  8935  axinf2  9087  zfinf2  9089  oemapso  9129  scottexs  9300  scott0s  9301  kardex  9307  karden  9308  dfac5lem1  9534  dfac5lem3  9536  kmlem15  9575  enfin2i  9732  fin23lem34  9757  brdom7disj  9942  fpwwe2lem12  10052  fpwwe2lem13  10053  axgroth5  10235  grothprim  10245  addsrpr  10486  mulsrpr  10487  mulgt0sr  10516  addcnsr  10546  mulcnsr  10547  ltresr  10551  axcnre  10575  1re  10630  ssxr  10699  infrenegsup  11611  nnwos  12303  zmin  12332  xrnemnf  12500  xrnepnf  12501  xmullem  12645  xmulcom  12647  xmulneg1  12650  xmulf  12653  xrinfmss2  12692  elfzuzb  12896  fzass4  12940  seqof  13423  hashbclem  13806  hashfacen  13808  xpcogend  14325  trclublem  14346  rexanre  14698  caubnd  14710  o1lo1  14886  rpnnen2lem12  15570  lcmcllem  15930  lcmftp  15970  lcmfunsnlem2  15974  isprm3  16017  prmreclem2  16243  4sqlem12  16282  isffth2  17178  fucinv  17235  lublecllem  17590  oduglb  17741  odulub  17743  issubm  17960  issubmd  17963  0subm  17974  insubm  17975  sursubmefmnd  18053  injsubmefmnd  18054  smndex1mgm  18064  isnsg2  18300  cycsubm  18337  oppgid  18476  symgfixf1  18557  pmtrrn2  18580  lsmdisjr  18802  lsmhash  18823  gsumcom3  19091  dprd0  19146  issrg  19250  dvdsrtr  19398  isirred2  19447  lss1d  19728  lspsolvlem  19907  lbsextlem2  19924  cnfldfunALT  20104  unocv  20369  iunocv  20370  evlsval  20758  mpomatmul  21051  cpmidpmat  21478  tgval2  21561  fctop  21609  ppttop  21612  epttop  21614  cnnei  21887  2ndcctbss  22060  txuni2  22170  txbas  22172  ptbasin  22182  txdis1cn  22240  xkococnlem  22264  opnfbas  22447  fgcl  22483  fbasrn  22489  filuni  22490  cfinfil  22498  csdfil  22499  fin1aufil  22537  rnelfmlem  22557  fmfnfmlem3  22561  txflf  22611  xmeterval  23039  reconn  23433  iimulcl  23542  isclmp  23702  iscau3  23882  rrxmvallem  24008  minveclem3  24033  pmltpc  24054  ovolfcl  24070  ismbl  24130  dyaddisj  24200  iblre  24397  plyun0  24794  logfaclbnd  25806  lgslem3  25883  lgsdir2lem5  25913  tgjustf  26267  ishpg  26553  usgrexmpllem  27050  nb3grpr2  27173  vtxd0nedgb  27278  wlk1walk  27428  clwlkcompbp  27571  wwlknllvtx  27632  wwlksonvtx  27641  wspthnonp  27645  wwlksn0s  27647  wwlksnndef  27691  2wlkdlem8  27719  elwwlks2s3  27737  clwwlkf1  27834  clwwlknonccat  27881  clwwlknon2x  27888  3pthdlem1  27949  upgr4cycl4dv4e  27970  frgr2wwlk1  28114  frgrreg  28179  ajfval  28592  issh  28991  chcon2i  29247  chcon3i  29249  spanuni  29327  5oalem7  29443  3oalem3  29447  pjin2i  29976  pjin3i  29977  cvnbtwn4  30072  mdslj1i  30102  mdslj2i  30103  mdslmd1i  30112  chrelat4i  30156  chirredi  30177  cdj3i  30224  rmoun  30265  difrab2  30268  eqdif  30290  inpr0  30304  iuninc  30324  fcoinvbr  30371  suppss2f  30398  fmptdF  30419  disjdsct  30462  cnvoprabOLD  30482  f1od2  30483  hashxpe  30555  tosglblem  30682  mgcval  30695  pmtrprfv2  30782  ssmxidllem  31049  ccfldextdgrr  31145  ordtconnlem1  31277  esumpfinvalf  31445  esum2dlem  31461  measiuns  31586  eulerpartlemt0  31737  eulerpartlemr  31742  eulerpartlemn  31749  ballotlem2  31856  ballotlemodife  31865  bnj887  32146  bnj976  32159  bnj1385  32214  bnj153  32262  bnj543  32275  bnj607  32298  bnj882  32308  bnj916  32315  bnj983  32333  derangenlem  32531  pconnconn  32591  fmlaomn0  32750  fmla0disjsuc  32758  fmlasucdisj  32759  elmpst  32896  dftr6  33099  dffr5  33102  dfpo2  33104  fundmpss  33122  elpotr  33139  soseq  33209  frrlem9  33244  fprlem1  33250  frrlem15  33255  nocvxmin  33361  sltrec  33391  brtxp  33454  brpprod  33459  brsset  33463  idsset  33464  dfon3  33466  ellimits  33484  dffun10  33488  elfuns  33489  brcart  33506  brimg  33511  brapply  33512  brcap  33514  brsuccf  33515  funpartfun  33517  dfrecs2  33524  dfrdg4  33525  altopthc  33545  altopthd  33546  altopelaltxp  33550  outsideoftr  33703  trer  33777  neibastop1  33820  neifg  33832  df3nandALT1  33860  imnand2  33863  eliminable-abelab  34308  bj-eldiag2  34592  bj-imdiridlem  34600  bj-opabco  34603  bj-xpcossxp  34604  topdifinfeq  34767  relowlssretop  34780  relowlpssretop  34781  wl-cases2-dnf  34917  wl-dfreusb  35022  wl-dfreuv  35023  wl-dfrabv  35027  poimirlem30  35087  poimirlem32  35089  ismblfin  35098  mbfposadd  35104  inixp  35166  elghomOLD  35325  keridl  35470  smprngopr  35490  sbcani  35546  an2anr  35658  inxpxrn  35803  dfcoss2  35821  1cossres  35834  dfcoels  35835  br1cossinres  35847  br1cossinidres  35849  br1cossincnvepres  35850  br1cossxrnidres  35851  br1cossxrncnvepres  35852  cosscnvssid3  35876  coss0  35879  cossid  35880  trcoss  35882  eleccossin  35883  dfssr2  35899  br1cossxrncnvssrres  35908  refsymrels3  35962  refsymrel2  35963  refsymrel3  35964  elrefsymrels3  35966  dfeqvrel2  35985  dfeqvrel3  35986  redundeq1  36024  redundpbi1  36026  dfmember3  36068  eqvreldmqs  36069  dfeldisj3  36112  prtlem10  36161  prter1  36175  lcvbr3  36319  isopos  36476  llnexatN  36817  snatpsubN  37046  pclclN  37187  pclfinN  37196  lhpocnel2  37315  cdlemk19w  38268  dih1dimatlem  38625  psspwb  39408  mzpclall  39668  mzpincl  39675  mzpindd  39687  2nn0ind  39886  dford4  39970  wopprc  39971  islmodfg  40013  isdomn3  40148  ifpan123g  40167  ifpan23  40168  ifpnot23  40186  ifpdfxor  40195  ifpidg  40199  ifpid1g  40202  ifpim23g  40203  ifpim123g  40208  ifpim1g  40209  ifp1bi  40210  ifpimimb  40212  ifpororb  40213  ifpor123g  40216  ifpbibib  40218  rp-isfinite6  40226  alephiso2  40257  undmrnresiss  40304  cotrintab  40314  brtrclfv2  40428  dfxor4  40467  snhesn  40487  dffrege76  40640  uneqsn  40726  expandan  40996  ismnuprim  41002  nzin  41022  onfrALTlem5  41248  onfrALTlem4  41249  undif3VD  41588  onfrALTlem5VD  41591  onfrALTlem4VD  41592  ndisj2  41685  rexabsle  42056  ellimcabssub0  42259  limsupre2mpt  42372  limsupre3  42375  limsupre3mpt  42376  limsupre3uz  42378  limsupreuz  42379  liminfreuz  42445  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  smflim  43410  smflim2  43437  smflimsuplem1  43451  smflimsup  43459  2reu8i  43669  ichan  43972  issubmgm  44409  rabsubmgmd  44411  2zlidl  44558  mndpsuppss  44773  islininds2  44893  zlmodzxzldeplem3  44911  2itscp  45195  alsi-no-surprise  45324