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  2344  aaan  2367  sbnf2  2392  cbveuvw  2635  cbveuw  2636  cbveuALT  2638  2mo2  2677  2eu4  2684  sbabel  2959  neanior  3053  r19.26m  3126  reeanlem  3238  rexeqbii  3339  reu5  3373  cbvreuw  3397  cgsex4g  3503  reu2  3690  reu3  3692  2reu5a  3709  2reu5lem3  3722  2reu1  3852  eqss  3953  unss  4143  ralunb  4150  ssin  4191  undi  4238  indifdi  4247  undif3  4253  inab  4262  difab  4263  reuss2  4279  reupick  4282  2reu4lem  4486  reuprg  4671  sstp  4803  tpss  4804  prneimg  4821  prneimg2  4822  prnebg  4823  uniinOLD  4899  intun  4947  disjiun  5099  disjxiun  5108  brin  5165  brdif  5166  ssext  5437  pweqb  5439  opthg2  5463  copsex4g  5480  propeqop  5492  eqopab2bw  5535  eqopab2b  5539  pwin  5554  pofun  5589  dffr6  5619  wetrep  5656  elxp3  5729  soinxp  5745  weinxp  5748  csbxp  5764  relun  5800  inopab  5818  difopab  5819  inxp  5820  opelco2g  5855  cnvco  5877  dmin  5903  restidsing  6057  intasym  6117  asymref  6118  asymref2  6119  cnvdif  6142  xpnz  6158  difxp  6163  xpdifid  6167  xpdifcnvepel  6168  xp11  6175  dfco2  6248  cnvpo  6292  cnvso  6293  xpco  6294  reu3op  6297  dfpo2  6301  dffun4  6553  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  7135  f13dfv  7281  dff1o6  7282  isotr  7343  eqoprab2bw  7489  eqoprab2b  7490  fvmpopr2d  7581  porpss  7734  epweon  7780  onsucb  7819  resf1extb  7937  elxp6  8026  dfoprab3  8057  opiota  8062  poxp  8130  soxp  8131  poxp2  8145  xpord2pred  8147  xpord2indlem  8149  xpord3pred  8154  xpord3inddlem  8156  soseq  8161  suppvalbr  8166  brtpos2  8234  frrlem9  8297  fprlem1  8303  tfrlem7  8376  dfer2  8701  eqer  8737  iiner  8793  uniinqs  8801  brecop  8814  eroveu  8816  erovlem  8817  fsetexb  8867  mapval2  8876  ixpin  8927  boxriin  8944  brsdom  8977  xpcomco  9062  xpassen  9066  sbthlem9  9090  sbthlem10  9091  brsdom2  9096  ssenen  9146  sbthfilem  9189  dffi3  9398  dfsup2  9411  infcllem  9455  axinf2  9616  zfinf2  9618  oemapso  9658  ttrcltr  9692  frrlem15  9736  scottexsOLD  9879  scott0bsOLD  9881  kardexOLD  9894  kardenOLD  9896  dfac5lem1  10123  dfac5lem3  10125  kmlem15  10164  enfin2i  10320  fin23lem34  10345  brdom7disj  10530  fpwwe2lem11  10643  fpwwe2lem12  10644  axgroth5  10826  grothprim  10836  addsrpr  11077  mulsrpr  11078  mulgt0sr  11107  addcnsr  11137  mulcnsr  11138  ltresr  11142  axcnre  11166  ssxr  11296  infrenegsup  12215  nnwos  12957  zmin  12986  xrnemnf  13160  xrnepnf  13161  xmullem  13308  xmulcom  13310  xmulneg1  13313  xmulf  13316  xrinfmss2  13355  elfzuzb  13564  fzass4  13609  seqof  14115  hashbclem  14509  hashfacen  14511  xpcogend  15037  trclublem  15058  rexanre  15424  caubnd  15436  o1lo1  15614  rpnnen2lem12  16305  lcmcllem  16678  lcmftp  16718  lcmfunsnlem2  16722  isprm3  16765  prmreclem2  17001  4sqlem12  17040  catcone0  17767  isffth2  17999  fucinv  18057  lublecllem  18438  odulub  18485  oduglb  18487  issubmgm  18794  rabsubmgmd  18796  mndpsuppss  18862  issubm  18900  issubmd  18903  0subm  18915  insubm  18916  sursubmefmnd  18994  injsubmefmnd  18995  smndex1mgm  19008  degenmgm  19039  degenmgm2  19042  isnsg2  19268  cycsubm  19319  oppgid  19472  symgfixf1  19553  pmtrrn2  19576  lsmdisjr  19800  lsmhash  19821  gsumcom3  20094  dprd0  20149  issrg  20316  dvdsrtr  20498  isirred2  20551  isdomn3  20865  opprdomnb  20867  isdomn4r  20869  lss1d  21136  lspsolvlem  21318  lbsextlem2  21335  ssdifidllem  21536  cnfldfun  21588  unocv  21882  iunocv  21883  evlsval  22289  mpomatmul  22655  cpmidpmat  23082  tgval2  23165  fctop  23213  ppttop  23216  epttop  23218  cnnei  23491  2ndcctbss  23665  txuni2  23775  txbas  23777  ptbasin  23787  txdis1cn  23845  xkococnlem  23869  opnfbas  24052  fgcl  24088  fbasrn  24094  filuni  24095  cfinfil  24103  csdfil  24104  fin1aufil  24142  rnelfmlem  24162  fmfnfmlem3  24166  txflf  24216  xmeterval  24642  reconn  25039  iimulcl  25149  isclmp  25309  iscau3  25490  rrxmvallem  25616  minveclem3  25641  pmltpc  25662  ovolfcl  25678  ismbl  25738  dyaddisj  25808  iblre  26006  plyun0  26407  logfaclbnd  27439  lgslem3  27516  lgsdir2lem5  27546  nosupinfsep  27949  ltsrec  28047  madebdaylemlrcut  28145  addsproplem2  28216  addsuniflem  28247  negsproplem2  28275  negsid  28287  mulsproplem5  28366  mulsproplem6  28367  mulsproplem7  28368  mulsproplem8  28369  mulsproplem9  28370  mulsuniflem  28395  precsexlem9  28461  precsexlem10  28462  ons2ind  28521  nnaddscl  28592  nnmulscl  28593  zaddscl  28640  zsoring  28655  recut  28740  readdscl  28745  remulscl  28748  tgjustf  28795  ishpg  29094  usgrexmpllem  29670  nb3grpr2  29793  vtxd0nedgb  29898  wlk1walk  30048  clwlkcompbp  30198  wwlknllvtx  30264  wwlksonvtx  30273  wspthnonp  30277  wwlksn0s  30279  wwlksnndef  30323  2wlkdlem8  30351  elwwlks2s3  30369  clwwlkf1  30469  clwwlknonccat  30516  clwwlknon2x  30523  3pthdlem1  30588  upgr4cycl4dv4e  30609  frgr2wwlk1  30753  frgrreg  30818  ajfval  31234  issh  31633  chcon2i  31889  chcon3i  31891  spanuni  31969  5oalem7  32085  3oalem3  32089  pjin2i  32618  pjin3i  32619  cvnbtwn4  32714  mdslj1i  32744  mdslj2i  32745  mdslmd1i  32754  chrelat4i  32798  chirredi  32819  cdj3i  32866  rmoun  32913  difrab2  32917  eqdif  32938  inpr0  32951  iuninc  32978  fcoinvbr  33023  suppss2f  33056  fmptdf2  33074  disjdsct  33121  f1od2  33136  hashxpe  33224  tosglblem  33360  mgcval  33373  pmtrprfv2  33474  elrgspnlem2  33629  ssmxidllem  33822  ccfldextdgrr  34128  fldext2chn  34184  ordtconnlem1  34380  esumpfinvalf  34532  esum2dlem  34548  measiuns  34674  eulerpartlemt0  34826  eulerpartlemr  34831  eulerpartlemn  34838  ballotlem2  34946  ballotlemodife  34955  bnj887  35221  bnj976  35233  bnj1385  35287  bnj153  35335  bnj543  35348  bnj607  35371  bnj882  35381  bnj916  35388  bnj983  35406  axreg  35599  axregscl  35600  axregs  35611  onvfowev  35659  derangenlem  35702  pconnconn  35762  fmlaomn0  35921  fmla0disjsuc  35929  fmlasucdisj  35930  elmpst  36067  xpab  36257  dftr6  36282  dffr5  36285  fundmpss  36298  elpotr  36310  brtxp  36409  brpprod  36414  brsset  36418  idsset  36419  dfon3  36421  ellimits  36439  dffun10  36443  elfuns  36444  brcart  36461  brimg  36466  brapply  36467  brcap  36469  lemsuccf  36470  funpartfun  36474  dfrecs2  36481  dfrdg4  36482  altopthc  36502  altopthd  36503  altopelaltxp  36507  outsideoftr  36660  rmoeqbii  36759  reueqbii  36761  rabeqbii  36765  riotaeqbii  36769  ixpeq1i  36771  cbvixpvw2  36816  cbvprodvw2  36818  trer  36886  neibastop1  36929  neifg  36941  df3nandALT1  36969  imnand2  36972  axtco  37041  regsfromregtco  37108  regsfromunir1  37110  mh-prprimbi  37113  eliminable-abelab  37564  bj-eldiag2  37880  bj-imdiridlem  37888  bj-opabco  37891  bj-xpcossxp  37892  topdifinfeq  38055  relowlssretop  38068  relowlpssretop  38069  wl-cases2-dnf  38226  poimirlem30  38360  poimirlem32  38362  ismblfin  38371  mbfposadd  38377  inixp  38439  elghomOLD  38598  keridl  38743  smprngopr  38763  sbcani  38817  inxpxrn  39127  dfcoss2  39212  cosscnv  39215  coss1cnvres  39216  coss2cnvepres  39217  1cossres  39228  dfcoels  39229  trressn  39244  br1cossinres  39246  br1cossinidres  39248  br1cossincnvepres  39249  br1cossxrnidres  39250  br1cossxrncnvepres  39251  cosscnvssid3  39275  coss0  39278  cossid  39279  trcoss  39281  eleccossin  39282  dfssr2  39288  br1cossxrncnvssrres  39297  refsymrels3  39359  refsymrel2  39360  refsymrel3  39361  elrefsymrels3  39363  dfeqvrel2  39383  dfeqvrel3  39384  redundeq1  39422  redundpbi1  39424  dfcomember3  39468  eqvreldmqs  39469  eqvreldmqs2  39470  dfeldisj3  39520  eldisjdmqsim  39526  eldisjn0elb  39554  antisymrelres  39575  dfmembpart2  39582  prtlem10  39699  prter1  39713  lcvbr3  39857  isopos  40014  llnexatN  40355  snatpsubN  40584  pclclN  40725  pclfinN  40734  lhpocnel2  40853  cdlemk19w  41806  dih1dimatlem  42163  psspwb  43059  redvmptabs  43181  mzpclall  43518  mzpincl  43525  mzpindd  43537  2nn0ind  43732  dford4  43816  wopprc  43817  islmodfg  43856  ifpan123g  44245  ifpan23  44246  ifpnot23  44264  ifpdfxor  44273  ifpidg  44277  ifpid1g  44280  ifpim23g  44281  ifpim123g  44286  ifpim1g  44287  ifp1bi  44288  ifpimimb  44290  ifpororb  44291  ifpor123g  44294  ifpbibib  44296  rp-isfinite6  44304  alephiso2  44344  undmrnresiss  44390  cotrintab  44400  brtrclfv2  44513  dfxor4  44552  snhesn  44572  dffrege76  44725  uneqsn  44811  expandan  45058  ismnuprim  45064  nzin  45088  onfrALTlem5  45311  onfrALTlem4  45312  undif3VD  45650  onfrALTlem5VD  45653  onfrALTlem4VD  45654  dfac5prim  45759  wfaxpr  45767  brpermmodel  45772  permac8prim  45783  ndisj2  45831  rexabsle  46193  ellimcabssub0  46393  limsupre2mpt  46504  limsupre3  46507  limsupre3mpt  46508  limsupre3uz  46510  limsupreuz  46511  liminfreuz  46577  fourierdlem103  46983  fourierdlem104  46984  fourierdlem112  46992  smflim  47551  smflim2  47580  smflimsuplem1  47594  smflimsup  47602  cfsetsnfsetf1  47856  2reu8i  47910  ichan  48264  clnbgrsym  48663  dfnbgr6  48682  upgrimpthslem2  48733  isgrlim  48807  usgrexmpl2trifr  48862  pgnbgreunbgrlem5  48948  pgnbgreunbgr  48950  2zlidl  49064  smprngprmrng  49163  islininds2  49323  zlmodzxzldeplem3  49341  2itscp  49620  reutruALT  49642  iinxp  49668  0funclem  49923  fucofulem2  50148  fuco2el  50149  catcinv  50236  2arwcatlem1  50432  dfrals2  50627  alsbii  50637  ralsbii  50638  cbvals  50642  als-no-surprise  50643  rals-no-surprise  50644  dfralseu2  50660  alseubii  50669  ralseubii  50670