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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anbi12ci  629  an2anr  636  ordi  1007  ordir  1008  orddi  1011  pm5.17  1013  xor  1016  cases2  1047  3anbi123i  1154  an6  1444  nanbi  1496  cadan  1605  nic-axALT  1670  19.43OLD  1880  sbbi  2306  aaan  2331  sbnf2  2358  eubii  2582  cbveuvw  2602  cbveuw  2603  cbveuALT  2605  2mo2  2644  2eu4  2652  sbabel  2935  sbabelOLD  2936  neanior  3032  r19.26m  3107  reeanlem  3225  2ralorOLD  3229  rexeqbii  3342  reu5  3379  cbvreuw  3407  cgsex4g  3525  reu2  3733  reu3  3735  2reu5a  3752  2reu5lem3  3765  2reu1  3905  eqss  4010  unss  4199  ralunb  4206  ssin  4246  undi  4290  indifdi  4299  undif3  4305  inab  4314  difab  4315  reuss2  4331  reupick  4334  2reu4lem  4527  reuprg  4707  sstp  4840  tpss  4841  prneimg  4858  prneimg2  4859  prnebg  4860  uniin  4935  intun  4984  disjiun  5135  disjxiun  5144  brin  5199  brdif  5200  ssext  5464  pweqb  5466  opthg2  5489  copsex4g  5504  propeqop  5516  eqopab2bw  5557  eqopab2b  5561  pwin  5578  pofun  5614  dffr6  5643  wetrep  5681  elxp3  5754  soinxp  5769  weinxp  5772  csbxp  5787  relun  5823  inopab  5841  difopab  5842  difopabOLD  5843  inxp  5844  inxpOLD  5845  opelco2g  5880  cnvco  5898  dmin  5924  restidsing  6072  intasym  6137  asymref  6138  asymref2  6139  cnvdif  6165  xpnz  6180  difxp  6185  xpdifid  6189  xp11  6196  dfco2  6266  relssdmrnOLD  6290  cnvpo  6308  cnvso  6309  xpco  6310  reu3op  6313  dfpo2  6317  dffun4  6578  funun  6613  fun11  6641  fununi  6642  imadif  6651  fnres  6695  mptfnf  6703  fnopabg  6705  fun  6770  fin  6788  dff1o2  6853  brprcneu  6896  brprcneuALT  6897  dffv2  7003  fsn  7154  f13dfv  7293  dff1o6  7294  isotr  7355  eqoprab2bw  7502  eqoprab2b  7503  fvmpopr2d  7594  porpss  7745  epweon  7793  onsucb  7836  elxp6  8046  dfoprab3  8077  opiota  8082  poxp  8151  soxp  8152  poxp2  8166  xpord2pred  8168  xpord2indlem  8170  xpord3pred  8175  xpord3inddlem  8177  soseq  8182  suppvalbr  8187  brtpos2  8255  frrlem9  8317  fprlem1  8323  wfrlem5OLD  8351  wfrfunOLD  8357  tfrlem7  8421  dfer2  8744  eqer  8779  iiner  8827  uniinqs  8835  brecop  8848  eroveu  8850  erovlem  8851  fsetexb  8902  mapval2  8910  ixpin  8961  boxriin  8978  brsdom  9013  xpcomco  9100  xpassen  9104  sbthlem9  9129  sbthlem10  9130  brsdom2  9135  ssenen  9189  sbthfilem  9235  dffi3  9468  dfsup2  9481  infcllem  9524  axinf2  9677  zfinf2  9679  oemapso  9719  ttrcltr  9753  frrlem15  9794  scottexs  9924  scott0s  9925  kardex  9931  karden  9932  dfac5lem1  10160  dfac5lem3  10162  kmlem15  10202  enfin2i  10358  fin23lem34  10383  brdom7disj  10568  fpwwe2lem11  10678  fpwwe2lem12  10679  axgroth5  10861  grothprim  10871  addsrpr  11112  mulsrpr  11113  mulgt0sr  11142  addcnsr  11172  mulcnsr  11173  ltresr  11177  axcnre  11201  1re  11258  ssxr  11327  infrenegsup  12248  nnwos  12954  zmin  12983  xrnemnf  13156  xrnepnf  13157  xmullem  13302  xmulcom  13304  xmulneg1  13307  xmulf  13310  xrinfmss2  13349  elfzuzb  13554  fzass4  13598  seqof  14096  hashbclem  14487  hashfacen  14489  xpcogend  15009  trclublem  15030  rexanre  15381  caubnd  15393  o1lo1  15569  rpnnen2lem12  16257  lcmcllem  16629  lcmftp  16669  lcmfunsnlem2  16673  isprm3  16716  prmreclem2  16950  4sqlem12  16989  catcone0  17731  isffth2  17969  fucinv  18029  lublecllem  18417  odulub  18464  oduglb  18466  issubmgm  18727  rabsubmgmd  18729  mndpsuppss  18790  issubm  18828  issubmd  18831  0subm  18842  insubm  18843  sursubmefmnd  18921  injsubmefmnd  18922  smndex1mgm  18932  isnsg2  19186  cycsubm  19232  oppgid  19389  symgfixf1  19469  pmtrrn2  19492  lsmdisjr  19716  lsmhash  19737  gsumcom3  20010  dprd0  20065  issrg  20205  dvdsrtr  20384  isirred2  20437  isdomn3  20731  opprdomnb  20733  isdomn4r  20735  lss1d  20978  lspsolvlem  21161  lbsextlem2  21178  cnfldfun  21395  cnfldfunOLD  21408  unocv  21715  iunocv  21716  evlsval  22127  mpomatmul  22467  cpmidpmat  22894  tgval2  22978  fctop  23026  ppttop  23029  epttop  23031  cnnei  23305  2ndcctbss  23478  txuni2  23588  txbas  23590  ptbasin  23600  txdis1cn  23658  xkococnlem  23682  opnfbas  23865  fgcl  23901  fbasrn  23907  filuni  23908  cfinfil  23916  csdfil  23917  fin1aufil  23955  rnelfmlem  23975  fmfnfmlem3  23979  txflf  24029  xmeterval  24457  reconn  24863  iimulcl  24979  isclmp  25143  iscau3  25325  rrxmvallem  25451  minveclem3  25476  pmltpc  25498  ovolfcl  25514  ismbl  25574  dyaddisj  25644  iblre  25843  plyun0  26250  logfaclbnd  27280  lgslem3  27357  lgsdir2lem5  27387  nosupinfsep  27791  nocvxmin  27837  sltrec  27879  madebdaylemlrcut  27951  addsproplem2  28017  addsuniflem  28048  negsproplem2  28075  negsid  28087  mulsproplem5  28160  mulsproplem6  28161  mulsproplem7  28162  mulsproplem8  28163  mulsproplem9  28164  mulsuniflem  28189  precsexlem9  28253  precsexlem10  28254  nnaddscl  28363  nnmulscl  28364  zaddscl  28394  recut  28442  0reno  28443  readdscl  28445  remulscl  28448  tgjustf  28495  ishpg  28781  usgrexmpllem  29291  nb3grpr2  29414  vtxd0nedgb  29520  wlk1walk  29671  clwlkcompbp  29814  wwlknllvtx  29875  wwlksonvtx  29884  wspthnonp  29888  wwlksn0s  29890  wwlksnndef  29934  2wlkdlem8  29962  elwwlks2s3  29980  clwwlkf1  30077  clwwlknonccat  30124  clwwlknon2x  30131  3pthdlem1  30192  upgr4cycl4dv4e  30213  frgr2wwlk1  30357  frgrreg  30422  ajfval  30837  issh  31236  chcon2i  31492  chcon3i  31494  spanuni  31572  5oalem7  31688  3oalem3  31692  pjin2i  32221  pjin3i  32222  cvnbtwn4  32317  mdslj1i  32347  mdslj2i  32348  mdslmd1i  32357  chrelat4i  32401  chirredi  32422  cdj3i  32469  rmoun  32521  difrab2  32525  eqdif  32546  inpr0  32557  iuninc  32580  fcoinvbr  32624  suppss2f  32654  fmptdF  32672  disjdsct  32717  cnvoprabOLD  32737  f1od2  32738  hashxpe  32816  tosglblem  32948  mgcval  32961  pmtrprfv2  33090  elrgspnlem2  33232  ssdifidllem  33463  ssmxidllem  33480  ccfldextdgrr  33696  ordtconnlem1  33884  esumpfinvalf  34056  esum2dlem  34072  measiuns  34197  eulerpartlemt0  34350  eulerpartlemr  34355  eulerpartlemn  34362  ballotlem2  34469  ballotlemodife  34478  bnj887  34757  bnj976  34769  bnj1385  34824  bnj153  34872  bnj543  34885  bnj607  34908  bnj882  34918  bnj916  34925  bnj983  34943  derangenlem  35155  pconnconn  35215  fmlaomn0  35374  fmla0disjsuc  35382  fmlasucdisj  35383  elmpst  35520  xpab  35705  dftr6  35730  dffr5  35733  fundmpss  35747  elpotr  35762  brtxp  35861  brpprod  35866  brsset  35870  idsset  35871  dfon3  35873  ellimits  35891  dffun10  35895  elfuns  35896  brcart  35913  brimg  35918  brapply  35919  brcap  35921  brsuccf  35922  funpartfun  35924  dfrecs2  35931  dfrdg4  35932  altopthc  35952  altopthd  35953  altopelaltxp  35957  outsideoftr  36110  rmoeqbii  36169  reueqbii  36171  rabeqbii  36175  riotaeqbii  36179  ixpeq1i  36181  cbvixpvw2  36227  cbvprodvw2  36229  trer  36298  neibastop1  36341  neifg  36353  df3nandALT1  36381  imnand2  36384  eliminable-abelab  36852  bj-eldiag2  37159  bj-imdiridlem  37167  bj-opabco  37170  bj-xpcossxp  37171  topdifinfeq  37332  relowlssretop  37345  relowlpssretop  37346  wl-cases2-dnf  37492  poimirlem30  37636  poimirlem32  37638  ismblfin  37647  mbfposadd  37653  inixp  37714  elghomOLD  37873  keridl  38018  smprngopr  38038  sbcani  38094  inxpxrn  38376  dfcoss2  38394  cosscnv  38397  coss1cnvres  38398  coss2cnvepres  38399  1cossres  38410  dfcoels  38411  trressn  38426  br1cossinres  38428  br1cossinidres  38430  br1cossincnvepres  38431  br1cossxrnidres  38432  br1cossxrncnvepres  38433  cosscnvssid3  38457  coss0  38460  cossid  38461  trcoss  38463  eleccossin  38464  dfssr2  38480  br1cossxrncnvssrres  38489  refsymrels3  38547  refsymrel2  38548  refsymrel3  38549  elrefsymrels3  38551  dfeqvrel2  38571  dfeqvrel3  38572  redundeq1  38610  redundpbi1  38612  dfcomember3  38655  eqvreldmqs  38656  eqvreldmqs2  38657  dfeldisj3  38700  eldisjn0elb  38726  antisymrelres  38744  dfmembpart2  38751  prtlem10  38846  prter1  38860  lcvbr3  39004  isopos  39161  llnexatN  39503  snatpsubN  39732  pclclN  39873  pclfinN  39882  lhpocnel2  40001  cdlemk19w  40954  dih1dimatlem  41311  psspwb  42245  redvmptabs  42368  mzpclall  42714  mzpincl  42721  mzpindd  42733  2nn0ind  42933  dford4  43017  wopprc  43018  islmodfg  43057  ifpan123g  43448  ifpan23  43449  ifpnot23  43467  ifpdfxor  43476  ifpidg  43480  ifpid1g  43483  ifpim23g  43484  ifpim123g  43489  ifpim1g  43490  ifp1bi  43491  ifpimimb  43493  ifpororb  43494  ifpor123g  43497  ifpbibib  43499  rp-isfinite6  43507  alephiso2  43547  undmrnresiss  43593  cotrintab  43603  brtrclfv2  43716  dfxor4  43755  snhesn  43775  dffrege76  43928  uneqsn  44014  expandan  44283  ismnuprim  44289  nzin  44313  onfrALTlem5  44539  onfrALTlem4  44540  undif3VD  44879  onfrALTlem5VD  44882  onfrALTlem4VD  44883  wfaxpr  44951  ndisj2  44990  rexabsle  45368  ellimcabssub0  45572  limsupre2mpt  45685  limsupre3  45688  limsupre3mpt  45689  limsupre3uz  45691  limsupreuz  45692  liminfreuz  45758  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  smflim  46732  smflim2  46761  smflimsuplem1  46775  smflimsup  46783  cfsetsnfsetf1  47008  2reu8i  47062  ichan  47379  clnbgrsym  47761  dfnbgr6  47780  isgrlim  47884  usgrexmpl2trifr  47931  2zlidl  48083  islininds2  48329  zlmodzxzldeplem3  48347  2itscp  48630  reutruALT  48653  alsi-no-surprise  49026