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  2341  aaan  2363  sbnf2  2388  cbveuvw  2631  cbveuw  2632  cbveuALT  2634  2mo2  2673  2eu4  2680  sbabel  2955  neanior  3049  r19.26m  3122  reeanlem  3234  rexeqbii  3334  reu5  3368  cbvreuw  3392  cgsex4g  3497  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  5422  pweqb  5424  opthg2  5448  copsex4g  5467  propeqop  5479  eqopab2bw  5523  eqopab2b  5527  pwin  5542  pofun  5577  dffr6  5607  wetrep  5644  elxp3  5717  soinxp  5733  weinxp  5736  csbxp  5752  relun  5789  inopab  5807  difopab  5808  inxp  5809  opelco2g  5845  cnvco  5867  dmin  5893  restidsing  6045  intasym  6109  asymref  6110  asymref2  6111  cnvdif  6134  xpnz  6150  difxp  6155  xpdifid  6159  xpdifcnvepel  6160  xp11  6167  dfco2  6246  cnvpo  6290  cnvso  6291  xpco  6292  reu3op  6295  dfpo2  6299  dffun4  6551  funun  6586  fun11  6614  fununi  6615  imadif  6624  fnres  6666  mptfnf  6674  fnopabg  6676  fun  6744  fin  6762  dff1o2  6830  brprcneu  6875  brprcneuALT  6876  dffv2  6980  fsn  7136  f13dfv  7282  dff1o6  7283  isotr  7344  eqoprab2bw  7490  eqoprab2b  7491  fvmpopr2d  7582  porpss  7743  epweon  7789  onsucb  7828  resf1extb  7946  elxp6  8035  dfoprab3  8065  opiota  8070  poxp  8140  soxp  8141  poxp2  8160  xpord2pred  8162  xpord2indlem  8164  xpord3pred  8169  xpord3inddlem  8171  soseq  8176  suppvalbr  8181  brtpos2  8249  frrlem9  8312  fprlem1  8318  tfrlem7  8391  dfer2  8718  eqer  8754  iiner  8810  uniinqs  8818  brecop  8831  eroveu  8833  erovlem  8834  fsetexb  8886  mapval2  8900  ixpin  8951  boxriin  8968  brsdom  9001  xpcomco  9086  xpassen  9090  sbthlem9  9114  sbthlem10  9115  brsdom2  9120  ssenen  9170  sbthfilem  9213  dffi3  9423  dfsup2  9436  infcllem  9480  axinf2  9641  zfinf2  9643  oemapso  9683  ttrcltr  9717  frrlem15  9761  scottexsOLD  9943  scott0bsOLD  9945  kardexOLD  9958  kardenOLD  9960  dfac5lem1  10202  dfac5lem3  10204  kmlem15  10243  enfin2i  10399  fin23lem34  10424  brdom7disj  10610  fpwwe2lem11  10726  fpwwe2lem12  10727  axgroth5  10909  grothprim  10919  addsrpr  11160  mulsrpr  11161  mulgt0sr  11190  addcnsr  11220  mulcnsr  11221  ltresr  11225  axcnre  11249  ssxr  11379  infrenegsup  12300  nnwos  13042  zmin  13071  xrnemnf  13246  xrnepnf  13247  xmullem  13394  xmulcom  13396  xmulneg1  13399  xmulf  13402  xrinfmss2  13441  elfzuzb  13650  fzass4  13696  seqof  14202  hashbclem  14597  hashfacen  14599  xpcogend  15127  trclublem  15148  rexanre  15514  caubnd  15526  o1lo1  15704  rpnnen2lem12  16393  lcmcllem  16771  lcmftp  16811  lcmfunsnlem2  16815  isprm3  16858  prmreclem2  17095  4sqlem12  17134  catcone0  17861  isffth2  18093  fucinv  18151  lublecllem  18532  odulub  18579  oduglb  18581  issubmgm  18891  rabsubmgmd  18893  mndpsuppss  18959  issubm  18998  issubmd  19001  0subm  19013  insubm  19014  sursubmefmnd  19092  injsubmefmnd  19093  smndex1mgm  19106  degenmgm  19137  degenmgm2  19140  isnsg2  19366  cycsubm  19417  oppgid  19570  symgfixf1  19651  pmtrrn2  19674  lsmdisjr  19898  lsmhash  19919  gsumcom3  20192  dprd0  20247  issrg  20414  dvdsrtr  20598  isirred2  20651  isdomn3  20966  opprdomnb  20968  isdomn4r  20970  lss1d  21238  lspsolvlem  21420  lbsextlem2  21437  ssdifidllem  21640  cnfldfun  21692  unocv  21986  iunocv  21987  evlsval  22395  mpomatmul  22761  cpmidpmat  23191  tgval2  23274  fctop  23322  ppttop  23325  epttop  23327  cnnei  23600  2ndcctbss  23774  txuni2  23884  txbas  23886  ptbasin  23896  txdis1cn  23954  xkococnlem  23978  opnfbas  24161  fgcl  24197  fbasrn  24203  filuni  24204  cfinfil  24212  csdfil  24213  fin1aufil  24251  rnelfmlem  24271  fmfnfmlem3  24275  txflf  24325  xmeterval  24751  reconn  25148  iimulcl  25258  isclmp  25418  iscau3  25599  rrxmvallem  25725  minveclem3  25750  pmltpc  25771  ovolfcl  25787  ismbl  25847  dyaddisj  25917  iblre  26114  plyun0  26515  logfaclbnd  27549  lgslem3  27626  lgsdir2lem5  27656  nosupinfsep  28089  ltsrec  28187  madebdaylemlrcut  28285  addsproplem2  28356  addsuniflem  28387  negsproplem2  28415  negsid  28427  mulsproplem5  28506  mulsproplem6  28507  mulsproplem7  28508  mulsproplem8  28509  mulsproplem9  28510  mulsuniflem  28535  precsexlem9  28601  precsexlem10  28602  ons2ind  28661  nnaddscl  28732  nnmulscl  28733  zaddscl  28780  zsoring  28795  recut  28880  readdscl  28885  remulscl  28888  tgjustf  28935  ishpg  29237  usgrexmpllem  29841  nb3grpr2  29964  vtxd0nedgb  30069  wlk1walk  30219  clwlkcompbp  30369  wwlknllvtx  30435  wwlksonvtx  30444  wspthnonp  30448  wwlksn0s  30450  wwlksnndef  30494  2wlkdlem8  30522  elwwlks2s3  30540  clwwlkf1  30640  clwwlknonccat  30687  clwwlknon2x  30694  3pthdlem1  30765  upgr4cycl4dv4e  30786  frgr2wwlk1  30930  frgrreg  30995  ajfval  31411  issh  31810  chcon2i  32066  chcon3i  32068  spanuni  32146  5oalem7  32262  3oalem3  32266  pjin2i  32795  pjin3i  32796  cvnbtwn4  32891  mdslj1i  32921  mdslj2i  32922  mdslmd1i  32931  chrelat4i  32975  chirredi  32996  cdj3i  33043  rmoun  33090  difrab2  33094  eqdif  33115  inpr0  33128  iuninc  33155  fcoinvbr  33199  suppss2f  33232  fmptdf2  33250  disjdsct  33296  f1od2  33311  hashxpe  33399  tosglblem  33535  mgcval  33548  pmtrprfv2  33649  elrgspnlem2  33804  ssmxidllem  33998  ccfldextdgrr  34304  fldext2chn  34360  ordtconnlem1  34556  esumpfinvalf  34708  esum2dlem  34724  measiuns  34850  eulerpartlemt0  35001  eulerpartlemr  35006  eulerpartlemn  35013  ballotlem2  35121  ballotlemodife  35130  bnj887  35396  bnj976  35408  bnj1385  35462  bnj153  35510  bnj543  35523  bnj607  35546  bnj882  35556  bnj916  35563  bnj983  35581  axreg  35795  axregscl  35796  axregs  35807  onvfowev  35899  derangenlem  35936  pconnconn  35996  fmlaomn0  36155  fmla0disjsuc  36163  fmlasucdisj  36164  elmpst  36301  xpab  36491  dftr6  36516  dffr5  36519  fundmpss  36532  elpotr  36543  brtxp  36642  brpprod  36647  brsset  36651  idsset  36652  dfon3  36654  ellimits  36672  dffun10  36676  elfuns  36677  brcart  36694  brimg  36699  brapply  36700  brcap  36702  lemsuccf  36703  funpartfun  36707  dfrecs2  36714  dfrdg4  36715  altopthc  36736  altopthd  36737  altopelaltxp  36741  outsideoftr  36894  rmoeqbii  36977  reueqbii  36979  rabeqbii  36983  riotaeqbii  36987  ixpeq1i  36989  cbvixpvw2  37034  cbvprodvw2  37036  trer  37104  neibastop1  37147  neifg  37159  df3nandALT1  37187  imnand2  37190  axtco  37259  regsfromregtco  37326  regsfromunir1  37328  mh-prprimbi  37331  eliminable-abelab  37782  bj-eldiag2  38098  bj-imdiridlem  38106  bj-opabco  38109  bj-xpcossxp  38110  topdifinfeq  38273  relowlssretop  38286  relowlpssretop  38287  wl-cases2-dnf  38444  poimirlem30  38568  poimirlem32  38570  ismblfin  38579  mbfposadd  38585  inixp  38662  elghomOLD  38821  keridl  38966  smprngopr  38986  sbcani  39040  inxpxrn  39350  dfcoss2  39435  cosscnv  39438  coss1cnvres  39439  coss2cnvepres  39440  1cossres  39451  dfcoels  39452  trressn  39467  br1cossinres  39469  br1cossinidres  39471  br1cossincnvepres  39472  br1cossxrnidres  39473  br1cossxrncnvepres  39474  cosscnvssid3  39498  coss0  39501  cossid  39502  trcoss  39504  eleccossin  39505  dfssr2  39511  br1cossxrncnvssrres  39520  refsymrels3  39582  refsymrel2  39583  refsymrel3  39584  elrefsymrels3  39586  dfeqvrel2  39606  dfeqvrel3  39607  redundeq1  39645  redundpbi1  39647  dfcomember3  39691  eqvreldmqs  39692  eqvreldmqs2  39693  dfeldisj3  39743  eldisjdmqsim  39749  eldisjn0elb  39777  antisymrelres  39798  dfmembpart2  39805  prtlem10  39922  prter1  39936  lcvbr3  40080  isopos  40237  llnexatN  40578  snatpsubN  40807  pclclN  40948  pclfinN  40957  lhpocnel2  41076  cdlemk19w  42029  dih1dimatlem  42386  psspwb  43282  redvmptabs  43411  mzpclall  43737  mzpincl  43744  mzpindd  43756  2nn0ind  43951  dford4  44035  wopprc  44036  islmodfg  44070  ifpan123g  44459  ifpan23  44460  ifpnot23  44478  ifpdfxor  44487  ifpidg  44491  ifpid1g  44494  ifpim23g  44495  ifpim123g  44500  ifpim1g  44501  ifp1bi  44502  ifpimimb  44504  ifpororb  44505  ifpor123g  44508  ifpbibib  44510  rp-isfinite6  44518  alephiso2  44558  undmrnresiss  44603  cotrintab  44613  brtrclfv2  44726  dfxor4  44765  snhesn  44785  dffrege76  44938  uneqsn  45024  expandan  45271  ismnuprim  45277  nzin  45301  onfrALTlem5  45524  onfrALTlem4  45525  undif3VD  45863  onfrALTlem5VD  45866  onfrALTlem4VD  45867  dfac5prim  45979  wfaxpr  45987  brpermmodel  45992  permac8prim  46003  ndisj2  46067  rexabsle  46428  ellimcabssub0  46628  limsupre2mpt  46739  limsupre3  46742  limsupre3mpt  46743  limsupre3uz  46745  limsupreuz  46746  liminfreuz  46812  fourierdlem103  47218  fourierdlem104  47219  fourierdlem112  47227  smflim  47786  smflim2  47815  smflimsuplem1  47829  smflimsup  47837  cfsetsnfsetf1  48128  2reu8i  48182  ichan  48536  clnbgrsym  48935  dfnbgr6  48954  upgrimpthslem2  49005  isgrlim  49079  usgrexmpl2trifr  49134  pgnbgreunbgrlem5  49220  pgnbgreunbgr  49222  2zlidl  49336  smprngprmrng  49435  islininds2  49595  zlmodzxzldeplem3  49613  2itscp  49892  reutruALT  49914  iinxp  49940  0funclem  50193  fucofulem2  50418  fuco2el  50419  catcinv  50506  2arwcatlem1  50702  dfrals2  50885  alsbii  50895  ralsbii  50896  cbvals  50900  als-no-surprise  50901  rals-no-surprise  50902  dfralseu2  50918  alseubii  50927  ralseubii  50928