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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anbi12ci  629  ordi  1002  ordir  1003  orddi  1006  pm5.17  1008  xor  1011  cases2  1042  3anbi123i  1151  an6  1441  nanbi  1490  cadan  1610  nic-axALT  1675  19.43OLD  1884  sbbi  2317  sbbivOLD  2327  sbnf2  2377  sbbiALT  2611  eubii  2670  cbveuALT  2692  2mo2  2732  2eu4  2739  sbabel  3015  neanior  3109  r19.26m  3173  rexeqbii  3326  reeanlem  3365  2ralor  3369  reu5  3430  reu2  3716  reu3  3718  2reu5a  3735  2reu5lem3  3748  2reu1  3881  eqss  3982  unss  4160  ralunb  4167  ssin  4207  undi  4251  indifdir  4260  undif3  4265  inab  4271  difab  4272  reuss2  4283  reupick  4287  2reu4lem  4465  reuprg  4639  sstp  4767  tpss  4768  prneimg  4785  prnebg  4786  uniin  4862  intun  4908  intpr  4909  disjiun  5053  disjxiun  5063  brin  5118  brdif  5119  ssext  5347  pweqb  5349  opthg2  5371  copsex4g  5385  propeqop  5397  eqopab2bw  5435  eqopab2b  5439  pwin  5454  pofun  5491  wetrep  5548  elxp3  5618  soinxp  5633  weinxp  5636  csbxp  5650  relun  5684  inopab  5701  difopab  5702  inxp  5703  opelco2g  5738  cnvco  5756  dmin  5780  restidsing  5922  intasym  5975  asymref  5976  asymref2  5977  cnvdif  6002  xpnz  6016  difxp  6021  xpdifid  6025  xp11  6032  dfco2  6098  relssdmrn  6121  cnvpo  6138  cnvso  6139  xpco  6140  reu3op  6143  dffun4  6367  funun  6400  fun11  6428  fununi  6429  imadif  6438  fnres  6474  mptfnf  6483  fnopabg  6485  fun  6540  fin  6559  dff1o2  6620  brprcneu  6662  dffv2  6756  fsn  6897  f13dfv  7031  dff1o6  7032  isotr  7089  eqoprab2bw  7224  eqoprab2b  7225  porpss  7453  sucelon  7532  elxp6  7723  dfoprab3  7752  opiota  7757  poxp  7822  soxp  7823  suppvalbr  7834  brtpos2  7898  wfrlem5  7959  wfrfun  7965  tfrlem7  8019  dfer2  8290  eqer  8324  iiner  8369  uniinqs  8377  brecop  8390  eroveu  8392  erovlem  8393  mapval2  8436  ixpin  8487  boxriin  8504  brsdom  8532  xpcomco  8607  xpassen  8611  sbthlem9  8635  sbthlem10  8636  brsdom2  8641  ssenen  8691  unfi  8785  dffi3  8895  dfsup2  8908  infcllem  8951  axinf2  9103  zfinf2  9105  oemapso  9145  scottexs  9316  scott0s  9317  kardex  9323  karden  9324  dfac5lem1  9549  dfac5lem3  9551  kmlem15  9590  enfin2i  9743  fin23lem34  9768  brdom7disj  9953  fpwwe2lem12  10063  fpwwe2lem13  10064  axgroth5  10246  grothprim  10256  addsrpr  10497  mulsrpr  10498  mulgt0sr  10527  addcnsr  10557  mulcnsr  10558  ltresr  10562  axcnre  10586  1re  10641  ssxr  10710  infrenegsup  11624  nnwos  12316  zmin  12345  xrnemnf  12513  xrnepnf  12514  xmullem  12658  xmulcom  12660  xmulneg1  12663  xmulf  12666  xrinfmss2  12705  elfzuzb  12903  fzass4  12946  seqof  13428  hashbclem  13811  hashfacen  13813  xpcogend  14334  trclublem  14355  rexanre  14706  caubnd  14718  o1lo1  14894  rpnnen2lem12  15578  lcmcllem  15940  lcmftp  15980  lcmfunsnlem2  15984  isprm3  16027  prmreclem2  16253  4sqlem12  16292  isffth2  17186  fucinv  17243  lublecllem  17598  oduglb  17749  odulub  17751  issubm  17968  issubmd  17971  0subm  17982  insubm  17983  sursubmefmnd  18061  injsubmefmnd  18062  smndex1mgm  18072  isnsg2  18308  cycsubm  18345  oppgid  18484  symgfixf1  18565  pmtrrn2  18588  lsmdisjr  18810  lsmhash  18831  gsumcom3  19098  dprd0  19153  issrg  19257  dvdsrtr  19402  isirred2  19451  lss1d  19735  lspsolvlem  19914  lbsextlem2  19931  evlsval  20299  cnfldfunALT  20558  unocv  20824  iunocv  20825  mpomatmul  21055  cpmidpmat  21481  tgval2  21564  fctop  21612  ppttop  21615  epttop  21617  cnnei  21890  2ndcctbss  22063  txuni2  22173  txbas  22175  ptbasin  22185  txdis1cn  22243  xkococnlem  22267  opnfbas  22450  fgcl  22486  fbasrn  22492  filuni  22493  cfinfil  22501  csdfil  22502  fin1aufil  22540  rnelfmlem  22560  fmfnfmlem3  22564  txflf  22614  xmeterval  23042  reconn  23436  iimulcl  23541  isclmp  23701  iscau3  23881  rrxmvallem  24007  minveclem3  24032  pmltpc  24051  ovolfcl  24067  ismbl  24127  dyaddisj  24197  iblre  24394  plyun0  24787  logfaclbnd  25798  lgslem3  25875  lgsdir2lem5  25905  tgjustf  26259  ishpg  26545  usgrexmpllem  27042  nb3grpr2  27165  vtxd0nedgb  27270  wlk1walk  27420  clwlkcompbp  27563  wwlknllvtx  27624  wwlksonvtx  27633  wspthnonp  27637  wwlksn0s  27639  wwlksnndef  27683  wwlksnfiOLD  27685  2wlkdlem8  27712  elwwlks2s3  27730  clwwlkf1  27828  clwwlknonccat  27875  clwwlknon2x  27882  3pthdlem1  27943  upgr4cycl4dv4e  27964  frgr2wwlk1  28108  frgrreg  28173  ajfval  28586  issh  28985  chcon2i  29241  chcon3i  29243  spanuni  29321  5oalem7  29437  3oalem3  29441  pjin2i  29970  pjin3i  29971  cvnbtwn4  30066  mdslj1i  30096  mdslj2i  30097  mdslmd1i  30106  chrelat4i  30150  chirredi  30171  cdj3i  30218  rmoun  30258  difrab2  30261  eqdif  30281  inpr0  30292  iuninc  30312  fcoinvbr  30358  suppss2f  30384  fmptdF  30401  disjdsct  30438  cnvoprabOLD  30456  f1od2  30457  hashxpe  30529  tosglblem  30656  pmtrprfv2  30732  ssmxidllem  30978  ccfldextdgrr  31057  ordtconnlem1  31167  esumpfinvalf  31335  esum2dlem  31351  measiuns  31476  eulerpartlemt0  31627  eulerpartlemr  31632  eulerpartlemn  31639  ballotlem2  31746  ballotlemodife  31755  bnj887  32036  bnj976  32049  bnj1385  32104  bnj153  32152  bnj543  32165  bnj607  32188  bnj882  32198  bnj916  32205  bnj983  32223  derangenlem  32418  pconnconn  32478  fmlaomn0  32637  fmla0disjsuc  32645  fmlasucdisj  32646  elmpst  32783  dftr6  32986  dffr5  32989  dfpo2  32991  fundmpss  33009  elpotr  33026  soseq  33096  frrlem9  33131  fprlem1  33137  frrlem15  33142  nocvxmin  33248  sltrec  33278  brtxp  33341  brpprod  33346  brsset  33350  idsset  33351  dfon3  33353  ellimits  33371  dffun10  33375  elfuns  33376  brcart  33393  brimg  33398  brapply  33399  brcap  33401  brsuccf  33402  funpartfun  33404  dfrecs2  33411  dfrdg4  33412  altopthc  33432  altopthd  33433  altopelaltxp  33437  outsideoftr  33590  trer  33664  neibastop1  33707  neifg  33719  df3nandALT1  33747  imnand2  33750  bj-eldiag2  34472  bj-imdirid  34478  topdifinfeq  34634  relowlssretop  34647  relowlpssretop  34648  wl-cases2-dnf  34767  wl-dfreusb  34872  wl-dfreuv  34873  wl-dfrabv  34877  poimirlem30  34937  poimirlem32  34939  ismblfin  34948  mbfposadd  34954  inixp  35018  elghomOLD  35180  keridl  35325  smprngopr  35345  sbcani  35401  an2anr  35513  inxpxrn  35658  dfcoss2  35676  1cossres  35689  dfcoels  35690  br1cossinres  35702  br1cossinidres  35704  br1cossincnvepres  35705  br1cossxrnidres  35706  br1cossxrncnvepres  35707  cosscnvssid3  35731  coss0  35734  cossid  35735  trcoss  35737  eleccossin  35738  dfssr2  35754  br1cossxrncnvssrres  35763  refsymrels3  35817  refsymrel2  35818  refsymrel3  35819  elrefsymrels3  35821  dfeqvrel2  35840  dfeqvrel3  35841  redundeq1  35879  redundpbi1  35881  dfmember3  35923  eqvreldmqs  35924  dfeldisj3  35967  prtlem10  36016  prter1  36030  lcvbr3  36174  isopos  36331  llnexatN  36672  snatpsubN  36901  pclclN  37042  pclfinN  37051  lhpocnel2  37170  cdlemk19w  38123  dih1dimatlem  38480  psspwb  39163  mzpclall  39373  mzpincl  39380  mzpindd  39392  2nn0ind  39591  dford4  39675  wopprc  39676  islmodfg  39718  isdomn3  39853  ifpan123g  39873  ifpan23  39874  ifpdfbi  39888  ifpnot23  39893  ifpdfxor  39902  ifpidg  39906  ifpid1g  39909  ifpim23g  39910  ifpim123g  39915  ifpim1g  39916  ifp1bi  39917  ifpimimb  39919  ifpororb  39920  ifpor123g  39923  ifpbibib  39925  rp-isfinite6  39933  alephiso2  39966  undmrnresiss  40013  cotrintab  40023  brtrclfv2  40121  dfxor4  40160  snhesn  40181  dffrege76  40334  uneqsn  40422  expandan  40673  ismnuprim  40679  nzin  40699  onfrALTlem5  40925  onfrALTlem4  40926  undif3VD  41265  onfrALTlem5VD  41268  onfrALTlem4VD  41269  ndisj2  41362  rexabsle  41742  ellimcabssub0  41947  limsupre2mpt  42060  limsupre3  42063  limsupre3mpt  42064  limsupre3uz  42066  limsupreuz  42067  liminfreuz  42133  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  smflim  43102  smflim2  43129  smflimsuplem1  43143  smflimsup  43151  2reu8i  43361  ichan  43679  issubmgm  44105  rabsubmgmd  44107  2zlidl  44254  mndpsuppss  44468  islininds2  44588  zlmodzxzldeplem3  44606  2itscp  44817  alsi-no-surprise  44946