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  1155  an6  1446  nanbi  1499  cadan  1608  nic-axALT  1673  19.43OLD  1882  sbbi  2307  aaan  2331  sbnf2  2359  eubii  2583  cbveuvw  2603  cbveuw  2604  cbveuALT  2606  2mo2  2645  2eu4  2653  sbabel  2930  neanior  3024  r19.26m  3097  reeanlem  3215  2ralorOLD  3219  rexeqbii  3328  reu5  3365  cbvreuw  3393  cgsex4g  3511  reu2  3713  reu3  3715  2reu5a  3732  2reu5lem3  3745  2reu1  3877  eqss  3979  unss  4170  ralunb  4177  ssin  4219  undi  4265  indifdi  4274  undif3  4280  inab  4289  difab  4290  reuss2  4306  reupick  4309  2reu4lem  4502  reuprg  4683  sstp  4816  tpss  4817  prneimg  4834  prneimg2  4835  prnebg  4836  uniin  4911  intun  4960  disjiun  5111  disjxiun  5120  brin  5175  brdif  5176  ssext  5439  pweqb  5441  opthg2  5464  copsex4g  5480  propeqop  5492  eqopab2bw  5533  eqopab2b  5537  pwin  5554  pofun  5590  dffr6  5620  wetrep  5658  elxp3  5731  soinxp  5747  weinxp  5750  csbxp  5765  relun  5801  inopab  5819  difopab  5820  difopabOLD  5821  inxp  5822  inxpOLD  5823  opelco2g  5858  cnvco  5876  dmin  5902  restidsing  6051  intasym  6115  asymref  6116  asymref2  6117  cnvdif  6143  xpnz  6159  difxp  6164  xpdifid  6168  xp11  6175  dfco2  6245  relssdmrnOLD  6269  cnvpo  6287  cnvso  6288  xpco  6289  reu3op  6292  dfpo2  6296  dffun4  6557  funun  6592  fun11  6620  fununi  6621  imadif  6630  fnres  6675  mptfnf  6683  fnopabg  6685  fun  6750  fin  6768  dff1o2  6833  brprcneu  6876  brprcneuALT  6877  dffv2  6984  fsn  7135  f13dfv  7276  dff1o6  7277  isotr  7338  eqoprab2bw  7485  eqoprab2b  7486  fvmpopr2d  7577  porpss  7729  epweon  7777  onsucb  7819  resf1extb  7938  elxp6  8030  dfoprab3  8061  opiota  8066  poxp  8135  soxp  8136  poxp2  8150  xpord2pred  8152  xpord2indlem  8154  xpord3pred  8159  xpord3inddlem  8161  soseq  8166  suppvalbr  8171  brtpos2  8239  frrlem9  8301  fprlem1  8307  wfrlem5OLD  8335  wfrfunOLD  8341  tfrlem7  8405  dfer2  8728  eqer  8763  iiner  8811  uniinqs  8819  brecop  8832  eroveu  8834  erovlem  8835  fsetexb  8886  mapval2  8894  ixpin  8945  boxriin  8962  brsdom  8997  xpcomco  9084  xpassen  9088  sbthlem9  9113  sbthlem10  9114  brsdom2  9119  ssenen  9173  sbthfilem  9220  dffi3  9453  dfsup2  9466  infcllem  9509  axinf2  9662  zfinf2  9664  oemapso  9704  ttrcltr  9738  frrlem15  9779  scottexs  9909  scott0s  9910  kardex  9916  karden  9917  dfac5lem1  10145  dfac5lem3  10147  kmlem15  10187  enfin2i  10343  fin23lem34  10368  brdom7disj  10553  fpwwe2lem11  10663  fpwwe2lem12  10664  axgroth5  10846  grothprim  10856  addsrpr  11097  mulsrpr  11098  mulgt0sr  11127  addcnsr  11157  mulcnsr  11158  ltresr  11162  axcnre  11186  1re  11243  ssxr  11312  infrenegsup  12233  nnwos  12939  zmin  12968  xrnemnf  13141  xrnepnf  13142  xmullem  13288  xmulcom  13290  xmulneg1  13293  xmulf  13296  xrinfmss2  13335  elfzuzb  13540  fzass4  13584  seqof  14082  hashbclem  14474  hashfacen  14476  xpcogend  14996  trclublem  15017  rexanre  15368  caubnd  15380  o1lo1  15556  rpnnen2lem12  16244  lcmcllem  16616  lcmftp  16656  lcmfunsnlem2  16660  isprm3  16703  prmreclem2  16938  4sqlem12  16977  catcone0  17702  isffth2  17935  fucinv  17993  lublecllem  18375  odulub  18422  oduglb  18424  issubmgm  18685  rabsubmgmd  18687  mndpsuppss  18748  issubm  18786  issubmd  18789  0subm  18800  insubm  18801  sursubmefmnd  18879  injsubmefmnd  18880  smndex1mgm  18890  isnsg2  19144  cycsubm  19190  oppgid  19344  symgfixf1  19424  pmtrrn2  19447  lsmdisjr  19671  lsmhash  19692  gsumcom3  19965  dprd0  20020  issrg  20154  dvdsrtr  20337  isirred2  20390  isdomn3  20684  opprdomnb  20686  isdomn4r  20688  lss1d  20930  lspsolvlem  21113  lbsextlem2  21130  cnfldfun  21341  cnfldfunOLD  21354  unocv  21653  iunocv  21654  evlsval  22059  mpomatmul  22401  cpmidpmat  22828  tgval2  22911  fctop  22959  ppttop  22962  epttop  22964  cnnei  23237  2ndcctbss  23410  txuni2  23520  txbas  23522  ptbasin  23532  txdis1cn  23590  xkococnlem  23614  opnfbas  23797  fgcl  23833  fbasrn  23839  filuni  23840  cfinfil  23848  csdfil  23849  fin1aufil  23887  rnelfmlem  23907  fmfnfmlem3  23911  txflf  23961  xmeterval  24388  reconn  24787  iimulcl  24903  isclmp  25067  iscau3  25249  rrxmvallem  25375  minveclem3  25400  pmltpc  25422  ovolfcl  25438  ismbl  25498  dyaddisj  25568  iblre  25766  plyun0  26173  logfaclbnd  27203  lgslem3  27280  lgsdir2lem5  27310  nosupinfsep  27714  nocvxmin  27760  sltrec  27802  madebdaylemlrcut  27874  addsproplem2  27940  addsuniflem  27971  negsproplem2  27998  negsid  28010  mulsproplem5  28083  mulsproplem6  28084  mulsproplem7  28085  mulsproplem8  28086  mulsproplem9  28087  mulsuniflem  28112  precsexlem9  28176  precsexlem10  28177  nnaddscl  28286  nnmulscl  28287  zaddscl  28317  recut  28365  0reno  28366  readdscl  28368  remulscl  28371  tgjustf  28418  ishpg  28704  usgrexmpllem  29206  nb3grpr2  29329  vtxd0nedgb  29435  wlk1walk  29586  clwlkcompbp  29731  wwlknllvtx  29795  wwlksonvtx  29804  wspthnonp  29808  wwlksn0s  29810  wwlksnndef  29854  2wlkdlem8  29882  elwwlks2s3  29900  clwwlkf1  29997  clwwlknonccat  30044  clwwlknon2x  30051  3pthdlem1  30112  upgr4cycl4dv4e  30133  frgr2wwlk1  30277  frgrreg  30342  ajfval  30757  issh  31156  chcon2i  31412  chcon3i  31414  spanuni  31492  5oalem7  31608  3oalem3  31612  pjin2i  32141  pjin3i  32142  cvnbtwn4  32237  mdslj1i  32267  mdslj2i  32268  mdslmd1i  32277  chrelat4i  32321  chirredi  32342  cdj3i  32389  rmoun  32442  difrab2  32446  eqdif  32467  inpr0  32481  iuninc  32509  fcoinvbr  32554  suppss2f  32584  fmptdF  32602  disjdsct  32648  f1od2  32668  hashxpe  32755  tosglblem  32908  mgcval  32921  pmtrprfv2  33052  elrgspnlem2  33191  ssdifidllem  33424  ssmxidllem  33441  ccfldextdgrr  33664  fldext2chn  33713  ordtconnlem1  33898  esumpfinvalf  34052  esum2dlem  34068  measiuns  34193  eulerpartlemt0  34346  eulerpartlemr  34351  eulerpartlemn  34358  ballotlem2  34466  ballotlemodife  34475  bnj887  34754  bnj976  34766  bnj1385  34821  bnj153  34869  bnj543  34882  bnj607  34905  bnj882  34915  bnj916  34922  bnj983  34940  derangenlem  35151  pconnconn  35211  fmlaomn0  35370  fmla0disjsuc  35378  fmlasucdisj  35379  elmpst  35516  xpab  35701  dftr6  35726  dffr5  35729  fundmpss  35742  elpotr  35757  brtxp  35856  brpprod  35861  brsset  35865  idsset  35866  dfon3  35868  ellimits  35886  dffun10  35890  elfuns  35891  brcart  35908  brimg  35913  brapply  35914  brcap  35916  brsuccf  35917  funpartfun  35919  dfrecs2  35926  dfrdg4  35927  altopthc  35947  altopthd  35948  altopelaltxp  35952  outsideoftr  36105  rmoeqbii  36164  reueqbii  36166  rabeqbii  36170  riotaeqbii  36174  ixpeq1i  36176  cbvixpvw2  36221  cbvprodvw2  36223  trer  36292  neibastop1  36335  neifg  36347  df3nandALT1  36375  imnand2  36378  eliminable-abelab  36846  bj-eldiag2  37153  bj-imdiridlem  37161  bj-opabco  37164  bj-xpcossxp  37165  topdifinfeq  37326  relowlssretop  37339  relowlpssretop  37340  wl-cases2-dnf  37488  poimirlem30  37632  poimirlem32  37634  ismblfin  37643  mbfposadd  37649  inixp  37710  elghomOLD  37869  keridl  38014  smprngopr  38034  sbcani  38090  inxpxrn  38371  dfcoss2  38389  cosscnv  38392  coss1cnvres  38393  coss2cnvepres  38394  1cossres  38405  dfcoels  38406  trressn  38421  br1cossinres  38423  br1cossinidres  38425  br1cossincnvepres  38426  br1cossxrnidres  38427  br1cossxrncnvepres  38428  cosscnvssid3  38452  coss0  38455  cossid  38456  trcoss  38458  eleccossin  38459  dfssr2  38475  br1cossxrncnvssrres  38484  refsymrels3  38542  refsymrel2  38543  refsymrel3  38544  elrefsymrels3  38546  dfeqvrel2  38566  dfeqvrel3  38567  redundeq1  38605  redundpbi1  38607  dfcomember3  38650  eqvreldmqs  38651  eqvreldmqs2  38652  dfeldisj3  38695  eldisjn0elb  38721  antisymrelres  38739  dfmembpart2  38746  prtlem10  38841  prter1  38855  lcvbr3  38999  isopos  39156  llnexatN  39498  snatpsubN  39727  pclclN  39868  pclfinN  39877  lhpocnel2  39996  cdlemk19w  40949  dih1dimatlem  41306  psspwb  42242  redvmptabs  42369  mzpclall  42716  mzpincl  42723  mzpindd  42735  2nn0ind  42935  dford4  43019  wopprc  43020  islmodfg  43059  ifpan123g  43449  ifpan23  43450  ifpnot23  43468  ifpdfxor  43477  ifpidg  43481  ifpid1g  43484  ifpim23g  43485  ifpim123g  43490  ifpim1g  43491  ifp1bi  43492  ifpimimb  43494  ifpororb  43495  ifpor123g  43498  ifpbibib  43500  rp-isfinite6  43508  alephiso2  43548  undmrnresiss  43594  cotrintab  43604  brtrclfv2  43717  dfxor4  43756  snhesn  43776  dffrege76  43929  uneqsn  44015  expandan  44279  ismnuprim  44285  nzin  44309  onfrALTlem5  44534  onfrALTlem4  44535  undif3VD  44874  onfrALTlem5VD  44877  onfrALTlem4VD  44878  dfac5prim  44979  wfaxpr  44987  ndisj2  45028  rexabsle  45402  ellimcabssub0  45604  limsupre2mpt  45717  limsupre3  45720  limsupre3mpt  45721  limsupre3uz  45723  limsupreuz  45724  liminfreuz  45790  fourierdlem103  46196  fourierdlem104  46197  fourierdlem112  46205  smflim  46764  smflim2  46793  smflimsuplem1  46807  smflimsup  46815  cfsetsnfsetf1  47044  2reu8i  47098  ichan  47415  clnbgrsym  47797  dfnbgr6  47816  isgrlim  47922  usgrexmpl2trifr  47969  2zlidl  48129  islininds2  48374  zlmodzxzldeplem3  48392  2itscp  48675  reutruALT  48698  iinxp  48718  0funclem  48944  fucofulem2  49056  fuco2el  49057  alsi-no-surprise  49410