Theorem anbi12i 626

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 623	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	3	anbi2i 622	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
5	2, 4	bitri 274	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  627  ordi  1002  ordir  1003  orddi  1006  pm5.17  1008  xor  1011  cases2  1044  3anbi123i  1153  an6  1443  nanbi  1492  cadan  1612  nic-axALT  1678  19.43OLD  1887  sbbi  2308  sbnf2  2356  eubii  2585  cbveuvw  2606  cbveuw  2607  cbveuALT  2610  2mo2  2649  2eu4  2656  sbabel  2940  sbabelOLD  2941  neanior  3036  r19.26m  3097  rexeqbii  3255  reeanlem  3290  2ralorOLD  3295  reu5  3351  reu2  3655  reu3  3657  2reu5a  3674  2reu5lem3  3687  2reu1  3826  eqss  3932  ss2abdv  3993  unss  4114  ralunb  4121  ssin  4161  undi  4205  indifdi  4214  indifdirOLD  4216  undif3  4221  inab  4230  difab  4231  reuss2  4246  reupick  4249  2reu4lem  4453  reuprg  4636  sstp  4764  tpss  4765  prneimg  4782  prnebg  4783  uniin  4862  intun  4908  intprOLD  4911  disjiun  5057  disjxiun  5067  brin  5122  brdif  5123  ssext  5364  pweqb  5366  opthg2  5388  copsex4g  5403  propeqop  5415  eqopab2bw  5454  eqopab2b  5458  pwin  5474  pofun  5512  dffr6  5538  wetrep  5573  elxp3  5644  soinxp  5659  weinxp  5662  csbxp  5676  relun  5710  inopab  5728  difopab  5729  inxp  5730  opelco2g  5765  cnvco  5783  dmin  5809  restidsing  5951  intasym  6009  asymref  6010  asymref2  6011  cnvdif  6036  xpnz  6051  difxp  6056  xpdifid  6060  xp11  6067  dfco2  6138  relssdmrn  6161  cnvpo  6179  cnvso  6180  xpco  6181  reu3op  6184  dfpo2  6188  dffun4  6430  funun  6464  fun11  6492  fununi  6493  imadif  6502  fnres  6543  mptfnf  6552  fnopabg  6554  fun  6620  fin  6638  dff1o2  6705  brprcneu  6747  fvprc  6748  dffv2  6845  fsn  6989  f13dfv  7127  dff1o6  7128  isotr  7187  eqoprab2bw  7323  eqoprab2b  7324  fvmpopr2d  7412  porpss  7558  sucelon  7639  elxp6  7838  dfoprab3  7867  opiota  7872  poxp  7940  soxp  7941  suppvalbr  7952  brtpos2  8019  frrlem9  8081  fprlem1  8087  wfrlem5OLD  8115  wfrfunOLD  8121  tfrlem7  8185  dfer2  8457  eqer  8491  iiner  8536  uniinqs  8544  brecop  8557  eroveu  8559  erovlem  8560  fsetexb  8610  mapval2  8618  ixpin  8669  boxriin  8686  brsdom  8718  xpcomco  8802  xpassen  8806  sbthlem9  8831  sbthlem10  8832  brsdom2  8837  ssenen  8887  sbthfilem  8941  unfiOLD  9011  dffi3  9120  dfsup2  9133  infcllem  9176  axinf2  9328  zfinf2  9330  oemapso  9370  frrlem15  9446  scottexs  9576  scott0s  9577  kardex  9583  karden  9584  dfac5lem1  9810  dfac5lem3  9812  kmlem15  9851  enfin2i  10008  fin23lem34  10033  brdom7disj  10218  fpwwe2lem11  10328  fpwwe2lem12  10329  axgroth5  10511  grothprim  10521  addsrpr  10762  mulsrpr  10763  mulgt0sr  10792  addcnsr  10822  mulcnsr  10823  ltresr  10827  axcnre  10851  1re  10906  ssxr  10975  infrenegsup  11888  nnwos  12584  zmin  12613  xrnemnf  12782  xrnepnf  12783  xmullem  12927  xmulcom  12929  xmulneg1  12932  xmulf  12935  xrinfmss2  12974  elfzuzb  13179  fzass4  13223  seqof  13708  hashbclem  14092  hashfacen  14094  hashfacenOLD  14095  xpcogend  14613  trclublem  14634  rexanre  14986  caubnd  14998  o1lo1  15174  rpnnen2lem12  15862  lcmcllem  16229  lcmftp  16269  lcmfunsnlem2  16273  isprm3  16316  prmreclem2  16546  4sqlem12  16585  catcone0  17313  isffth2  17548  fucinv  17607  lublecllem  17993  odulub  18040  oduglb  18042  issubm  18357  issubmd  18360  0subm  18371  insubm  18372  sursubmefmnd  18450  injsubmefmnd  18451  smndex1mgm  18461  isnsg2  18699  cycsubm  18736  oppgid  18878  symgfixf1  18960  pmtrrn2  18983  lsmdisjr  19205  lsmhash  19226  gsumcom3  19494  dprd0  19549  issrg  19658  dvdsrtr  19809  isirred2  19858  lss1d  20140  lspsolvlem  20319  lbsextlem2  20336  cnfldfunALT  20523  unocv  20797  iunocv  20798  evlsval  21206  mpomatmul  21503  cpmidpmat  21930  tgval2  22014  fctop  22062  ppttop  22065  epttop  22067  cnnei  22341  2ndcctbss  22514  txuni2  22624  txbas  22626  ptbasin  22636  txdis1cn  22694  xkococnlem  22718  opnfbas  22901  fgcl  22937  fbasrn  22943  filuni  22944  cfinfil  22952  csdfil  22953  fin1aufil  22991  rnelfmlem  23011  fmfnfmlem3  23015  txflf  23065  xmeterval  23493  reconn  23897  iimulcl  24006  isclmp  24166  iscau3  24347  rrxmvallem  24473  minveclem3  24498  pmltpc  24519  ovolfcl  24535  ismbl  24595  dyaddisj  24665  iblre  24863  plyun0  25263  logfaclbnd  26275  lgslem3  26352  lgsdir2lem5  26382  tgjustf  26738  ishpg  27024  usgrexmpllem  27530  nb3grpr2  27653  vtxd0nedgb  27758  wlk1walk  27908  clwlkcompbp  28051  wwlknllvtx  28112  wwlksonvtx  28121  wspthnonp  28125  wwlksn0s  28127  wwlksnndef  28171  2wlkdlem8  28199  elwwlks2s3  28217  clwwlkf1  28314  clwwlknonccat  28361  clwwlknon2x  28368  3pthdlem1  28429  upgr4cycl4dv4e  28450  frgr2wwlk1  28594  frgrreg  28659  ajfval  29072  issh  29471  chcon2i  29727  chcon3i  29729  spanuni  29807  5oalem7  29923  3oalem3  29927  pjin2i  30456  pjin3i  30457  cvnbtwn4  30552  mdslj1i  30582  mdslj2i  30583  mdslmd1i  30592  chrelat4i  30636  chirredi  30657  cdj3i  30704  rmoun  30743  difrab2  30746  eqdif  30767  inpr0  30781  iuninc  30801  fcoinvbr  30848  suppss2f  30875  fmptdF  30895  disjdsct  30937  cnvoprabOLD  30957  f1od2  30958  hashxpe  31029  tosglblem  31154  mgcval  31167  pmtrprfv2  31259  ssmxidllem  31543  ccfldextdgrr  31644  ordtconnlem1  31776  esumpfinvalf  31944  esum2dlem  31960  measiuns  32085  eulerpartlemt0  32236  eulerpartlemr  32241  eulerpartlemn  32248  ballotlem2  32355  ballotlemodife  32364  bnj887  32645  bnj976  32657  bnj1385  32712  bnj153  32760  bnj543  32773  bnj607  32796  bnj882  32806  bnj916  32813  bnj983  32831  derangenlem  33033  pconnconn  33093  fmlaomn0  33252  fmla0disjsuc  33260  fmlasucdisj  33261  elmpst  33398  xpab  33579  dftr6  33624  dffr5  33627  fundmpss  33646  elpotr  33663  ttrcltr  33702  poxp2  33717  xpord2pred  33719  xpord2ind  33721  xpord3pred  33725  xpord3ind  33727  soseq  33730  nosupinfsep  33862  nocvxmin  33900  sltrec  33941  madebdaylemlrcut  34006  brtxp  34109  brpprod  34114  brsset  34118  idsset  34119  dfon3  34121  ellimits  34139  dffun10  34143  elfuns  34144  brcart  34161  brimg  34166  brapply  34167  brcap  34169  brsuccf  34170  funpartfun  34172  dfrecs2  34179  dfrdg4  34180  altopthc  34200  altopthd  34201  altopelaltxp  34205  outsideoftr  34358  trer  34432  neibastop1  34475  neifg  34487  df3nandALT1  34515  imnand2  34518  eliminable-abelab  34981  bj-eldiag2  35275  bj-imdiridlem  35283  bj-opabco  35286  bj-xpcossxp  35287  topdifinfeq  35448  relowlssretop  35461  relowlpssretop  35462  wl-cases2-dnf  35598  poimirlem30  35734  poimirlem32  35736  ismblfin  35745  mbfposadd  35751  inixp  35813  elghomOLD  35972  keridl  36117  smprngopr  36137  sbcani  36193  an2anr  36305  inxpxrn  36448  dfcoss2  36466  1cossres  36479  dfcoels  36480  br1cossinres  36492  br1cossinidres  36494  br1cossincnvepres  36495  br1cossxrnidres  36496  br1cossxrncnvepres  36497  cosscnvssid3  36521  coss0  36524  cossid  36525  trcoss  36527  eleccossin  36528  dfssr2  36544  br1cossxrncnvssrres  36553  refsymrels3  36607  refsymrel2  36608  refsymrel3  36609  elrefsymrels3  36611  dfeqvrel2  36630  dfeqvrel3  36631  redundeq1  36669  redundpbi1  36671  dfmember3  36713  eqvreldmqs  36714  dfeldisj3  36757  prtlem10  36806  prter1  36820  lcvbr3  36964  isopos  37121  llnexatN  37462  snatpsubN  37691  pclclN  37832  pclfinN  37841  lhpocnel2  37960  cdlemk19w  38913  dih1dimatlem  39270  psspwb  40129  mhphf  40208  mzpclall  40465  mzpincl  40472  mzpindd  40484  2nn0ind  40683  dford4  40767  wopprc  40768  islmodfg  40810  isdomn3  40945  ifpan123g  40964  ifpan23  40965  ifpnot23  40983  ifpdfxor  40992  ifpidg  40996  ifpid1g  40999  ifpim23g  41000  ifpim123g  41005  ifpim1g  41006  ifp1bi  41007  ifpimimb  41009  ifpororb  41010  ifpor123g  41013  ifpbibib  41015  rp-isfinite6  41023  alephiso2  41054  undmrnresiss  41101  cotrintab  41111  brtrclfv2  41224  dfxor4  41263  snhesn  41283  dffrege76  41436  uneqsn  41522  expandan  41795  ismnuprim  41801  nzin  41825  onfrALTlem5  42051  onfrALTlem4  42052  undif3VD  42391  onfrALTlem5VD  42394  onfrALTlem4VD  42395  ndisj2  42488  rexabsle  42849  ellimcabssub0  43048  limsupre2mpt  43161  limsupre3  43164  limsupre3mpt  43165  limsupre3uz  43167  limsupreuz  43168  liminfreuz  43234  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  smflim  44199  smflim2  44226  smflimsuplem1  44240  smflimsup  44248  cfsetsnfsetf1  44440  2reu8i  44492  ichan  44795  issubmgm  45231  rabsubmgmd  45233  2zlidl  45380  mndpsuppss  45595  islininds2  45713  zlmodzxzldeplem3  45731  2itscp  46015  reutruALT  46040  alsi-no-surprise  46386