Theorem anbi12i 640

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anbi12ci  641  an2anr  648  ordi  1023  ordir  1024  orddi  1027  pm5.17  1029  xor  1032  cases2  1063  3anbi123i  1173  an6  1474  nanbi  1530  cadan  1642  nic-axALT  1707  19.43OLD  1916  sbbi  2340  aaan  2362  sbnf2  2387  cbveuvw  2630  cbveuw  2631  cbveuALT  2633  2mo2  2672  2eu4  2679  sbabel  2954  neanior  3048  r19.26m  3121  reeanlem  3233  rexeqbii  3333  reu5  3367  cbvreuw  3391  cgsex4g  3496  reu2  3683  reu3  3685  2reu5a  3702  2reu5lem3  3715  2reu1  3845  eqss  3946  unss  4136  ralunb  4143  ssin  4184  undi  4231  indifdi  4240  undif3  4246  inab  4255  difab  4256  reuss2  4272  reupick  4275  2reu4lem  4479  reuprg  4664  sstp  4796  tpss  4797  prneimg  4814  prneimg2  4815  prnebg  4816  uniinOLD  4892  intun  4940  disjiun  5091  disjxiun  5100  brin  5157  brdif  5158  ssext  5429  pweqb  5431  opthg2  5455  copsex4g  5472  propeqop  5484  eqopab2bw  5527  eqopab2b  5531  pwin  5546  pofun  5581  dffr6  5611  wetrep  5648  elxp3  5721  soinxp  5737  weinxp  5740  csbxp  5756  relun  5792  inopab  5810  difopab  5811  inxp  5812  opelco2g  5847  cnvco  5869  dmin  5895  restidsing  6049  intasym  6109  asymref  6110  asymref2  6111  cnvdif  6134  xpnz  6151  difxp  6156  xpdifid  6160  xpdifcnvepel  6161  xp11  6168  dfco2  6241  cnvpo  6285  cnvso  6286  xpco  6287  reu3op  6290  dfpo2  6294  dffun4  6546  funun  6580  fun11  6608  fununi  6609  imadif  6618  fnres  6660  mptfnf  6668  fnopabg  6670  fun  6738  fin  6756  dff1o2  6824  brprcneu  6869  brprcneuALT  6870  dffv2  6974  fsn  7130  f13dfv  7276  dff1o6  7277  isotr  7338  eqoprab2bw  7484  eqoprab2b  7485  fvmpopr2d  7576  porpss  7729  epweon  7775  onsucb  7814  resf1extb  7932  elxp6  8021  dfoprab3  8052  opiota  8057  poxp  8127  soxp  8128  poxp2  8142  xpord2pred  8144  xpord2indlem  8146  xpord3pred  8151  xpord3inddlem  8153  soseq  8158  suppvalbr  8163  brtpos2  8231  frrlem9  8294  fprlem1  8300  tfrlem7  8373  dfer2  8700  eqer  8736  iiner  8792  uniinqs  8800  brecop  8813  eroveu  8815  erovlem  8816  fsetexb  8868  mapval2  8882  ixpin  8933  boxriin  8950  brsdom  8983  xpcomco  9068  xpassen  9072  sbthlem9  9096  sbthlem10  9097  brsdom2  9102  ssenen  9152  sbthfilem  9195  dffi3  9404  dfsup2  9417  infcllem  9461  axinf2  9622  zfinf2  9624  oemapso  9664  ttrcltr  9698  frrlem15  9742  scottexsOLD  9885  scott0bsOLD  9887  kardexOLD  9900  kardenOLD  9902  dfac5lem1  10129  dfac5lem3  10131  kmlem15  10170  enfin2i  10326  fin23lem34  10351  brdom7disj  10537  fpwwe2lem11  10653  fpwwe2lem12  10654  axgroth5  10836  grothprim  10846  addsrpr  11087  mulsrpr  11088  mulgt0sr  11117  addcnsr  11147  mulcnsr  11148  ltresr  11152  axcnre  11176  ssxr  11306  infrenegsup  12225  nnwos  12967  zmin  12996  xrnemnf  13171  xrnepnf  13172  xmullem  13319  xmulcom  13321  xmulneg1  13324  xmulf  13327  xrinfmss2  13366  elfzuzb  13575  fzass4  13620  seqof  14126  hashbclem  14520  hashfacen  14522  xpcogend  15050  trclublem  15071  rexanre  15437  caubnd  15449  o1lo1  15627  rpnnen2lem12  16316  lcmcllem  16689  lcmftp  16729  lcmfunsnlem2  16733  isprm3  16776  prmreclem2  17012  4sqlem12  17051  catcone0  17778  isffth2  18010  fucinv  18068  lublecllem  18449  odulub  18496  oduglb  18498  issubmgm  18807  rabsubmgmd  18809  mndpsuppss  18875  issubm  18914  issubmd  18917  0subm  18929  insubm  18930  sursubmefmnd  19008  injsubmefmnd  19009  smndex1mgm  19022  degenmgm  19053  degenmgm2  19056  isnsg2  19282  cycsubm  19333  oppgid  19486  symgfixf1  19567  pmtrrn2  19590  lsmdisjr  19814  lsmhash  19835  gsumcom3  20108  dprd0  20163  issrg  20330  dvdsrtr  20512  isirred2  20565  isdomn3  20879  opprdomnb  20881  isdomn4r  20883  lss1d  21150  lspsolvlem  21332  lbsextlem2  21349  ssdifidllem  21550  cnfldfun  21602  unocv  21896  iunocv  21897  evlsval  22305  mpomatmul  22671  cpmidpmat  23101  tgval2  23184  fctop  23232  ppttop  23235  epttop  23237  cnnei  23510  2ndcctbss  23684  txuni2  23794  txbas  23796  ptbasin  23806  txdis1cn  23864  xkococnlem  23888  opnfbas  24071  fgcl  24107  fbasrn  24113  filuni  24114  cfinfil  24122  csdfil  24123  fin1aufil  24161  rnelfmlem  24181  fmfnfmlem3  24185  txflf  24235  xmeterval  24661  reconn  25058  iimulcl  25168  isclmp  25328  iscau3  25509  rrxmvallem  25635  minveclem3  25660  pmltpc  25681  ovolfcl  25697  ismbl  25757  dyaddisj  25827  iblre  26024  plyun0  26425  logfaclbnd  27461  lgslem3  27538  lgsdir2lem5  27568  nosupinfsep  27971  ltsrec  28069  madebdaylemlrcut  28167  addsproplem2  28238  addsuniflem  28269  negsproplem2  28297  negsid  28309  mulsproplem5  28388  mulsproplem6  28389  mulsproplem7  28390  mulsproplem8  28391  mulsproplem9  28392  mulsuniflem  28417  precsexlem9  28483  precsexlem10  28484  ons2ind  28543  nnaddscl  28614  nnmulscl  28615  zaddscl  28662  zsoring  28677  recut  28762  readdscl  28767  remulscl  28770  tgjustf  28817  ishpg  29119  usgrexmpllem  29723  nb3grpr2  29846  vtxd0nedgb  29951  wlk1walk  30101  clwlkcompbp  30251  wwlknllvtx  30317  wwlksonvtx  30326  wspthnonp  30330  wwlksn0s  30332  wwlksnndef  30376  2wlkdlem8  30404  elwwlks2s3  30422  clwwlkf1  30522  clwwlknonccat  30569  clwwlknon2x  30576  3pthdlem1  30647  upgr4cycl4dv4e  30668  frgr2wwlk1  30812  frgrreg  30877  ajfval  31293  issh  31692  chcon2i  31948  chcon3i  31950  spanuni  32028  5oalem7  32144  3oalem3  32148  pjin2i  32677  pjin3i  32678  cvnbtwn4  32773  mdslj1i  32803  mdslj2i  32804  mdslmd1i  32813  chrelat4i  32857  chirredi  32878  cdj3i  32925  rmoun  32972  difrab2  32976  eqdif  32997  inpr0  33010  iuninc  33037  fcoinvbr  33081  suppss2f  33114  fmptdf2  33132  disjdsct  33178  f1od2  33193  hashxpe  33281  tosglblem  33417  mgcval  33430  pmtrprfv2  33531  elrgspnlem2  33686  ssmxidllem  33879  ccfldextdgrr  34185  fldext2chn  34241  ordtconnlem1  34437  esumpfinvalf  34589  esum2dlem  34605  measiuns  34731  eulerpartlemt0  34883  eulerpartlemr  34888  eulerpartlemn  34895  ballotlem2  35003  ballotlemodife  35012  bnj887  35278  bnj976  35290  bnj1385  35344  bnj153  35392  bnj543  35405  bnj607  35428  bnj882  35438  bnj916  35445  bnj983  35463  axreg  35656  axregscl  35657  axregs  35668  onvfowev  35716  derangenlem  35753  pconnconn  35813  fmlaomn0  35972  fmla0disjsuc  35980  fmlasucdisj  35981  elmpst  36118  xpab  36308  dftr6  36333  dffr5  36336  fundmpss  36349  elpotr  36361  brtxp  36460  brpprod  36465  brsset  36469  idsset  36470  dfon3  36472  ellimits  36490  dffun10  36494  elfuns  36495  brcart  36512  brimg  36517  brapply  36518  brcap  36520  lemsuccf  36521  funpartfun  36525  dfrecs2  36532  dfrdg4  36533  altopthc  36554  altopthd  36555  altopelaltxp  36559  outsideoftr  36712  rmoeqbii  36811  reueqbii  36813  rabeqbii  36817  riotaeqbii  36821  ixpeq1i  36823  cbvixpvw2  36868  cbvprodvw2  36870  trer  36938  neibastop1  36981  neifg  36993  df3nandALT1  37021  imnand2  37024  axtco  37093  regsfromregtco  37160  regsfromunir1  37162  mh-prprimbi  37165  eliminable-abelab  37616  bj-eldiag2  37932  bj-imdiridlem  37940  bj-opabco  37943  bj-xpcossxp  37944  topdifinfeq  38107  relowlssretop  38120  relowlpssretop  38121  wl-cases2-dnf  38278  poimirlem30  38402  poimirlem32  38404  ismblfin  38413  mbfposadd  38419  inixp  38481  elghomOLD  38640  keridl  38785  smprngopr  38805  sbcani  38859  inxpxrn  39169  dfcoss2  39254  cosscnv  39257  coss1cnvres  39258  coss2cnvepres  39259  1cossres  39270  dfcoels  39271  trressn  39286  br1cossinres  39288  br1cossinidres  39290  br1cossincnvepres  39291  br1cossxrnidres  39292  br1cossxrncnvepres  39293  cosscnvssid3  39317  coss0  39320  cossid  39321  trcoss  39323  eleccossin  39324  dfssr2  39330  br1cossxrncnvssrres  39339  refsymrels3  39401  refsymrel2  39402  refsymrel3  39403  elrefsymrels3  39405  dfeqvrel2  39425  dfeqvrel3  39426  redundeq1  39464  redundpbi1  39466  dfcomember3  39510  eqvreldmqs  39511  eqvreldmqs2  39512  dfeldisj3  39562  eldisjdmqsim  39568  eldisjn0elb  39596  antisymrelres  39617  dfmembpart2  39624  prtlem10  39741  prter1  39755  lcvbr3  39899  isopos  40056  llnexatN  40397  snatpsubN  40626  pclclN  40767  pclfinN  40776  lhpocnel2  40895  cdlemk19w  41848  dih1dimatlem  42205  psspwb  43101  redvmptabs  43238  mzpclall  43575  mzpincl  43582  mzpindd  43594  2nn0ind  43789  dford4  43873  wopprc  43874  islmodfg  43913  ifpan123g  44302  ifpan23  44303  ifpnot23  44321  ifpdfxor  44330  ifpidg  44334  ifpid1g  44337  ifpim23g  44338  ifpim123g  44343  ifpim1g  44344  ifp1bi  44345  ifpimimb  44347  ifpororb  44348  ifpor123g  44351  ifpbibib  44353  rp-isfinite6  44361  alephiso2  44401  undmrnresiss  44447  cotrintab  44457  brtrclfv2  44570  dfxor4  44609  snhesn  44629  dffrege76  44782  uneqsn  44868  expandan  45115  ismnuprim  45121  nzin  45145  onfrALTlem5  45368  onfrALTlem4  45369  undif3VD  45707  onfrALTlem5VD  45710  onfrALTlem4VD  45711  dfac5prim  45816  wfaxpr  45824  brpermmodel  45829  permac8prim  45840  ndisj2  45888  rexabsle  46250  ellimcabssub0  46450  limsupre2mpt  46561  limsupre3  46564  limsupre3mpt  46565  limsupre3uz  46567  limsupreuz  46568  liminfreuz  46634  fourierdlem103  47040  fourierdlem104  47041  fourierdlem112  47049  smflim  47608  smflim2  47637  smflimsuplem1  47651  smflimsup  47659  cfsetsnfsetf1  47950  2reu8i  48004  ichan  48358  clnbgrsym  48757  dfnbgr6  48776  upgrimpthslem2  48827  isgrlim  48901  usgrexmpl2trifr  48956  pgnbgreunbgrlem5  49042  pgnbgreunbgr  49044  2zlidl  49158  smprngprmrng  49257  islininds2  49417  zlmodzxzldeplem3  49435  2itscp  49714  reutruALT  49736  iinxp  49762  0funclem  50015  fucofulem2  50240  fuco2el  50241  catcinv  50328  2arwcatlem1  50524  dfrals2  50722  alsbii  50732  ralsbii  50733  cbvals  50737  als-no-surprise  50738  rals-no-surprise  50739  dfralseu2  50755  alseubii  50764  ralseubii  50765