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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  anbi12ci  628  ordi  1003  ordir  1004  orddi  1007  pm5.17  1009  xor  1012  cases2  1045  3anbi123i  1154  an6  1444  nanbi  1495  cadan  1611  nic-axALT  1677  19.43OLD  1887  sbbi  2306  aaan  2329  sbnf2  2357  eubii  2586  cbveuvw  2607  cbveuw  2608  cbveuALT  2611  2mo2  2650  2eu4  2657  sbabel  2942  sbabelOLD  2943  neanior  3038  r19.26m  3099  rexeqbii  3261  reeanlem  3293  2ralorOLD  3298  reu5  3362  cbvreuw  3377  reu2  3661  reu3  3663  2reu5a  3680  2reu5lem3  3693  2reu1  3831  eqss  3937  ss2abdv  3998  unss  4119  ralunb  4126  ssin  4165  undi  4209  indifdi  4218  indifdirOLD  4220  undif3  4225  inab  4234  difab  4235  reuss2  4250  reupick  4253  2reu4lem  4457  reuprg  4640  sstp  4768  tpss  4769  prneimg  4786  prnebg  4787  uniin  4866  intun  4912  intprOLD  4915  disjiun  5062  disjxiun  5072  brin  5127  brdif  5128  ssext  5371  pweqb  5373  opthg2  5395  copsex4g  5410  propeqop  5422  eqopab2bw  5462  eqopab2b  5466  pwin  5484  pofun  5522  dffr6  5548  wetrep  5583  elxp3  5654  soinxp  5669  weinxp  5672  csbxp  5687  relun  5723  inopab  5741  difopab  5742  difopabOLD  5743  inxp  5744  opelco2g  5779  cnvco  5797  dmin  5823  restidsing  5965  intasym  6025  asymref  6026  asymref2  6027  cnvdif  6052  xpnz  6067  difxp  6072  xpdifid  6076  xp11  6083  dfco2  6153  relssdmrn  6176  cnvpo  6194  cnvso  6195  xpco  6196  reu3op  6199  dfpo2  6203  dffun4  6452  funun  6487  fun11  6515  fununi  6516  imadif  6525  fnres  6568  mptfnf  6577  fnopabg  6579  fun  6645  fin  6663  dff1o2  6730  brprcneu  6773  brprcneuALT  6774  dffv2  6872  fsn  7016  f13dfv  7155  dff1o6  7156  isotr  7216  eqoprab2bw  7354  eqoprab2b  7355  fvmpopr2d  7443  porpss  7589  epweon  7634  sucelon  7673  elxp6  7874  dfoprab3  7903  opiota  7908  poxp  7978  soxp  7979  suppvalbr  7990  brtpos2  8057  frrlem9  8119  fprlem1  8125  wfrlem5OLD  8153  wfrfunOLD  8159  tfrlem7  8223  dfer2  8508  eqer  8542  iiner  8587  uniinqs  8595  brecop  8608  eroveu  8610  erovlem  8611  fsetexb  8661  mapval2  8669  ixpin  8720  boxriin  8737  brsdom  8772  xpcomco  8858  xpassen  8862  sbthlem9  8887  sbthlem10  8888  brsdom2  8893  ssenen  8947  sbthfilem  8993  unfiOLD  9090  dffi3  9199  dfsup2  9212  infcllem  9255  axinf2  9407  zfinf2  9409  oemapso  9449  ttrcltr  9483  frrlem15  9524  scottexs  9654  scott0s  9655  kardex  9661  karden  9662  dfac5lem1  9888  dfac5lem3  9890  kmlem15  9929  enfin2i  10086  fin23lem34  10111  brdom7disj  10296  fpwwe2lem11  10406  fpwwe2lem12  10407  axgroth5  10589  grothprim  10599  addsrpr  10840  mulsrpr  10841  mulgt0sr  10870  addcnsr  10900  mulcnsr  10901  ltresr  10905  axcnre  10929  1re  10984  ssxr  11053  infrenegsup  11967  nnwos  12664  zmin  12693  xrnemnf  12862  xrnepnf  12863  xmullem  13007  xmulcom  13009  xmulneg1  13012  xmulf  13015  xrinfmss2  13054  elfzuzb  13259  fzass4  13303  seqof  13789  hashbclem  14173  hashfacen  14175  hashfacenOLD  14176  xpcogend  14694  trclublem  14715  rexanre  15067  caubnd  15079  o1lo1  15255  rpnnen2lem12  15943  lcmcllem  16310  lcmftp  16350  lcmfunsnlem2  16354  isprm3  16397  prmreclem2  16627  4sqlem12  16666  catcone0  17405  isffth2  17641  fucinv  17700  lublecllem  18087  odulub  18134  oduglb  18136  issubm  18451  issubmd  18454  0subm  18465  insubm  18466  sursubmefmnd  18544  injsubmefmnd  18545  smndex1mgm  18555  isnsg2  18793  cycsubm  18830  oppgid  18972  symgfixf1  19054  pmtrrn2  19077  lsmdisjr  19299  lsmhash  19320  gsumcom3  19588  dprd0  19643  issrg  19752  dvdsrtr  19903  isirred2  19952  lss1d  20234  lspsolvlem  20413  lbsextlem2  20430  cnfldfun  20618  unocv  20894  iunocv  20895  evlsval  21305  mpomatmul  21604  cpmidpmat  22031  tgval2  22115  fctop  22163  ppttop  22166  epttop  22168  cnnei  22442  2ndcctbss  22615  txuni2  22725  txbas  22727  ptbasin  22737  txdis1cn  22795  xkococnlem  22819  opnfbas  23002  fgcl  23038  fbasrn  23044  filuni  23045  cfinfil  23053  csdfil  23054  fin1aufil  23092  rnelfmlem  23112  fmfnfmlem3  23116  txflf  23166  xmeterval  23594  reconn  24000  iimulcl  24109  isclmp  24269  iscau3  24451  rrxmvallem  24577  minveclem3  24602  pmltpc  24623  ovolfcl  24639  ismbl  24699  dyaddisj  24769  iblre  24967  plyun0  25367  logfaclbnd  26379  lgslem3  26456  lgsdir2lem5  26486  tgjustf  26843  ishpg  27129  usgrexmpllem  27636  nb3grpr2  27759  vtxd0nedgb  27864  wlk1walk  28015  clwlkcompbp  28159  wwlknllvtx  28220  wwlksonvtx  28229  wspthnonp  28233  wwlksn0s  28235  wwlksnndef  28279  2wlkdlem8  28307  elwwlks2s3  28325  clwwlkf1  28422  clwwlknonccat  28469  clwwlknon2x  28476  3pthdlem1  28537  upgr4cycl4dv4e  28558  frgr2wwlk1  28702  frgrreg  28767  ajfval  29180  issh  29579  chcon2i  29835  chcon3i  29837  spanuni  29915  5oalem7  30031  3oalem3  30035  pjin2i  30564  pjin3i  30565  cvnbtwn4  30660  mdslj1i  30690  mdslj2i  30691  mdslmd1i  30700  chrelat4i  30744  chirredi  30765  cdj3i  30812  rmoun  30851  difrab2  30854  eqdif  30875  inpr0  30889  iuninc  30909  fcoinvbr  30956  suppss2f  30983  fmptdF  31002  disjdsct  31044  cnvoprabOLD  31064  f1od2  31065  hashxpe  31136  tosglblem  31261  mgcval  31274  pmtrprfv2  31366  ssmxidllem  31650  ccfldextdgrr  31751  ordtconnlem1  31883  esumpfinvalf  32053  esum2dlem  32069  measiuns  32194  eulerpartlemt0  32345  eulerpartlemr  32350  eulerpartlemn  32357  ballotlem2  32464  ballotlemodife  32473  bnj887  32754  bnj976  32766  bnj1385  32821  bnj153  32869  bnj543  32882  bnj607  32905  bnj882  32915  bnj916  32922  bnj983  32940  derangenlem  33142  pconnconn  33202  fmlaomn0  33361  fmla0disjsuc  33369  fmlasucdisj  33370  elmpst  33507  xpab  33686  dftr6  33727  dffr5  33730  fundmpss  33749  elpotr  33766  poxp2  33799  xpord2pred  33801  xpord2ind  33803  xpord3pred  33807  xpord3ind  33809  soseq  33812  nosupinfsep  33944  nocvxmin  33982  sltrec  34023  madebdaylemlrcut  34088  brtxp  34191  brpprod  34196  brsset  34200  idsset  34201  dfon3  34203  ellimits  34221  dffun10  34225  elfuns  34226  brcart  34243  brimg  34248  brapply  34249  brcap  34251  brsuccf  34252  funpartfun  34254  dfrecs2  34261  dfrdg4  34262  altopthc  34282  altopthd  34283  altopelaltxp  34287  outsideoftr  34440  trer  34514  neibastop1  34557  neifg  34569  df3nandALT1  34597  imnand2  34600  eliminable-abelab  35063  bj-eldiag2  35357  bj-imdiridlem  35365  bj-opabco  35368  bj-xpcossxp  35369  topdifinfeq  35530  relowlssretop  35543  relowlpssretop  35544  wl-cases2-dnf  35680  poimirlem30  35816  poimirlem32  35818  ismblfin  35827  mbfposadd  35833  inixp  35895  elghomOLD  36054  keridl  36199  smprngopr  36219  sbcani  36275  an2anr  36387  inxpxrn  36528  dfcoss2  36546  1cossres  36559  dfcoels  36560  br1cossinres  36572  br1cossinidres  36574  br1cossincnvepres  36575  br1cossxrnidres  36576  br1cossxrncnvepres  36577  cosscnvssid3  36601  coss0  36604  cossid  36605  trcoss  36607  eleccossin  36608  dfssr2  36624  br1cossxrncnvssrres  36633  refsymrels3  36687  refsymrel2  36688  refsymrel3  36689  elrefsymrels3  36691  dfeqvrel2  36710  dfeqvrel3  36711  redundeq1  36749  redundpbi1  36751  dfmember3  36793  eqvreldmqs  36794  dfeldisj3  36837  prtlem10  36886  prter1  36900  lcvbr3  37044  isopos  37201  llnexatN  37542  snatpsubN  37771  pclclN  37912  pclfinN  37921  lhpocnel2  38040  cdlemk19w  38993  dih1dimatlem  39350  psspwb  40210  mhphf  40292  mzpclall  40556  mzpincl  40563  mzpindd  40575  2nn0ind  40774  dford4  40858  wopprc  40859  islmodfg  40901  isdomn3  41036  ifpan123g  41073  ifpan23  41074  ifpnot23  41092  ifpdfxor  41101  ifpidg  41105  ifpid1g  41108  ifpim23g  41109  ifpim123g  41114  ifpim1g  41115  ifp1bi  41116  ifpimimb  41118  ifpororb  41119  ifpor123g  41122  ifpbibib  41124  rp-isfinite6  41132  alephiso2  41172  undmrnresiss  41219  cotrintab  41229  brtrclfv2  41342  dfxor4  41381  snhesn  41401  dffrege76  41554  uneqsn  41640  expandan  41913  ismnuprim  41919  nzin  41943  onfrALTlem5  42169  onfrALTlem4  42170  undif3VD  42509  onfrALTlem5VD  42512  onfrALTlem4VD  42513  ndisj2  42606  rexabsle  42966  ellimcabssub0  43165  limsupre2mpt  43278  limsupre3  43281  limsupre3mpt  43282  limsupre3uz  43284  limsupreuz  43285  liminfreuz  43351  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  smflim  44322  smflim2  44350  smflimsuplem1  44364  smflimsup  44372  cfsetsnfsetf1  44564  2reu8i  44616  ichan  44918  issubmgm  45354  rabsubmgmd  45356  2zlidl  45503  mndpsuppss  45718  islininds2  45836  zlmodzxzldeplem3  45854  2itscp  46138  reutruALT  46163  alsi-no-surprise  46511