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  1447  nanbi  1501  cadan  1610  nic-axALT  1675  19.43OLD  1884  sbbi  2311  aaan  2335  sbnf2  2360  cbveuvw  2603  cbveuw  2604  cbveuALT  2606  2mo2  2645  2eu4  2653  sbabel  2929  neanior  3023  r19.26m  3093  reeanlem  3205  rexeqbii  3313  reu5  3350  cbvreuw  3374  cgsex4g  3485  reu2  3681  reu3  3683  2reu5a  3700  2reu5lem3  3713  2reu1  3845  eqss  3947  unss  4140  ralunb  4147  ssin  4189  undi  4235  indifdi  4244  undif3  4250  inab  4259  difab  4260  reuss2  4276  reupick  4279  2reu4lem  4474  reuprg  4658  sstp  4790  tpss  4791  prneimg  4808  prneimg2  4809  prnebg  4810  uniin  4885  intun  4933  disjiun  5084  disjxiun  5093  brin  5148  brdif  5149  ssext  5400  pweqb  5402  opthg2  5425  copsex4g  5441  propeqop  5453  eqopab2bw  5494  eqopab2b  5498  pwin  5513  pofun  5548  dffr6  5578  wetrep  5615  elxp3  5688  soinxp  5704  weinxp  5707  csbxp  5723  relun  5758  inopab  5776  difopab  5777  inxp  5778  inxpOLD  5779  opelco2g  5814  cnvco  5832  dmin  5858  restidsing  6010  intasym  6070  asymref  6071  asymref2  6072  cnvdif  6099  xpnz  6115  difxp  6120  xpdifid  6124  xp11  6131  dfco2  6201  cnvpo  6243  cnvso  6244  xpco  6245  reu3op  6248  dfpo2  6252  dffun4  6503  funun  6536  fun11  6564  fununi  6565  imadif  6574  fnres  6617  mptfnf  6625  fnopabg  6627  fun  6694  fin  6712  dff1o2  6777  brprcneu  6822  brprcneuALT  6823  dffv2  6927  fsn  7078  f13dfv  7218  dff1o6  7219  isotr  7280  eqoprab2bw  7426  eqoprab2b  7427  fvmpopr2d  7518  porpss  7670  epweon  7718  onsucb  7757  resf1extb  7874  elxp6  7965  dfoprab3  7996  opiota  8001  poxp  8068  soxp  8069  poxp2  8083  xpord2pred  8085  xpord2indlem  8087  xpord3pred  8092  xpord3inddlem  8094  soseq  8099  suppvalbr  8104  brtpos2  8172  frrlem9  8234  fprlem1  8240  tfrlem7  8312  dfer2  8634  eqer  8669  iiner  8724  uniinqs  8732  brecop  8745  eroveu  8747  erovlem  8748  fsetexb  8799  mapval2  8808  ixpin  8859  boxriin  8876  brsdom  8909  xpcomco  8993  xpassen  8997  sbthlem9  9021  sbthlem10  9022  brsdom2  9027  ssenen  9077  sbthfilem  9120  dffi3  9332  dfsup2  9345  infcllem  9389  axinf2  9547  zfinf2  9549  oemapso  9589  ttrcltr  9623  frrlem15  9667  scottexs  9797  scott0s  9798  kardex  9804  karden  9805  dfac5lem1  10031  dfac5lem3  10033  kmlem15  10073  enfin2i  10229  fin23lem34  10254  brdom7disj  10439  fpwwe2lem11  10550  fpwwe2lem12  10551  axgroth5  10733  grothprim  10743  addsrpr  10984  mulsrpr  10985  mulgt0sr  11014  addcnsr  11044  mulcnsr  11045  ltresr  11049  axcnre  11073  ssxr  11200  infrenegsup  12123  nnwos  12826  zmin  12855  xrnemnf  13029  xrnepnf  13030  xmullem  13177  xmulcom  13179  xmulneg1  13182  xmulf  13185  xrinfmss2  13224  elfzuzb  13432  fzass4  13476  seqof  13980  hashbclem  14373  hashfacen  14375  xpcogend  14895  trclublem  14916  rexanre  15268  caubnd  15280  o1lo1  15458  rpnnen2lem12  16148  lcmcllem  16521  lcmftp  16561  lcmfunsnlem2  16565  isprm3  16608  prmreclem2  16843  4sqlem12  16882  catcone0  17608  isffth2  17840  fucinv  17898  lublecllem  18279  odulub  18326  oduglb  18328  issubmgm  18625  rabsubmgmd  18627  mndpsuppss  18688  issubm  18726  issubmd  18729  0subm  18740  insubm  18741  sursubmefmnd  18819  injsubmefmnd  18820  smndex1mgm  18830  isnsg2  19083  cycsubm  19129  oppgid  19283  symgfixf1  19364  pmtrrn2  19387  lsmdisjr  19611  lsmhash  19632  gsumcom3  19905  dprd0  19960  issrg  20121  dvdsrtr  20302  isirred2  20355  isdomn3  20646  opprdomnb  20648  isdomn4r  20650  lss1d  20912  lspsolvlem  21095  lbsextlem2  21112  cnfldfun  21321  cnfldfunOLD  21334  unocv  21633  iunocv  21634  evlsval  22039  mpomatmul  22388  cpmidpmat  22815  tgval2  22898  fctop  22946  ppttop  22949  epttop  22951  cnnei  23224  2ndcctbss  23397  txuni2  23507  txbas  23509  ptbasin  23519  txdis1cn  23577  xkococnlem  23601  opnfbas  23784  fgcl  23820  fbasrn  23826  filuni  23827  cfinfil  23835  csdfil  23836  fin1aufil  23874  rnelfmlem  23894  fmfnfmlem3  23898  txflf  23948  xmeterval  24374  reconn  24771  iimulcl  24887  isclmp  25051  iscau3  25232  rrxmvallem  25358  minveclem3  25383  pmltpc  25405  ovolfcl  25421  ismbl  25481  dyaddisj  25551  iblre  25749  plyun0  26156  logfaclbnd  27187  lgslem3  27264  lgsdir2lem5  27294  nosupinfsep  27698  sltrec  27789  madebdaylemlrcut  27871  addsproplem2  27940  addsuniflem  27971  negsproplem2  27998  negsid  28010  mulsproplem5  28089  mulsproplem6  28090  mulsproplem7  28091  mulsproplem8  28092  mulsproplem9  28093  mulsuniflem  28118  precsexlem9  28183  precsexlem10  28184  nnaddscl  28306  nnmulscl  28307  zaddscl  28352  zsoring  28367  recut  28439  readdscl  28444  remulscl  28447  tgjustf  28494  ishpg  28780  usgrexmpllem  29282  nb3grpr2  29405  vtxd0nedgb  29511  wlk1walk  29661  clwlkcompbp  29804  wwlknllvtx  29868  wwlksonvtx  29877  wspthnonp  29881  wwlksn0s  29883  wwlksnndef  29927  2wlkdlem8  29955  elwwlks2s3  29973  clwwlkf1  30073  clwwlknonccat  30120  clwwlknon2x  30127  3pthdlem1  30188  upgr4cycl4dv4e  30209  frgr2wwlk1  30353  frgrreg  30418  ajfval  30833  issh  31232  chcon2i  31488  chcon3i  31490  spanuni  31568  5oalem7  31684  3oalem3  31688  pjin2i  32217  pjin3i  32218  cvnbtwn4  32313  mdslj1i  32343  mdslj2i  32344  mdslmd1i  32353  chrelat4i  32397  chirredi  32418  cdj3i  32465  rmoun  32517  difrab2  32521  eqdif  32543  inpr0  32556  iuninc  32584  fcoinvbr  32629  suppss2f  32665  fmptdF  32683  disjdsct  32731  f1od2  32747  hashxpe  32836  tosglblem  33005  mgcval  33018  pmtrprfv2  33119  elrgspnlem2  33274  ssdifidllem  33486  ssmxidllem  33503  ccfldextdgrr  33778  fldext2chn  33834  ordtconnlem1  34030  esumpfinvalf  34182  esum2dlem  34198  measiuns  34323  eulerpartlemt0  34475  eulerpartlemr  34480  eulerpartlemn  34487  ballotlem2  34595  ballotlemodife  34604  bnj887  34870  bnj976  34882  bnj1385  34937  bnj153  34985  bnj543  34998  bnj607  35021  bnj882  35031  bnj916  35038  bnj983  35056  axreg  35232  axregscl  35233  axregs  35244  derangenlem  35314  pconnconn  35374  fmlaomn0  35533  fmla0disjsuc  35541  fmlasucdisj  35542  elmpst  35679  xpab  35869  dftr6  35894  dffr5  35897  fundmpss  35910  elpotr  35922  brtxp  36021  brpprod  36026  brsset  36030  idsset  36031  dfon3  36033  ellimits  36051  dffun10  36055  elfuns  36056  brcart  36073  brimg  36078  brapply  36079  brcap  36081  lemsuccf  36082  funpartfun  36086  dfrecs2  36093  dfrdg4  36094  altopthc  36114  altopthd  36115  altopelaltxp  36119  outsideoftr  36272  rmoeqbii  36331  reueqbii  36333  rabeqbii  36337  riotaeqbii  36341  ixpeq1i  36343  cbvixpvw2  36388  cbvprodvw2  36390  trer  36459  neibastop1  36502  neifg  36514  df3nandALT1  36542  imnand2  36545  eliminable-abelab  37014  bj-eldiag2  37321  bj-imdiridlem  37329  bj-opabco  37332  bj-xpcossxp  37333  topdifinfeq  37494  relowlssretop  37507  relowlpssretop  37508  wl-cases2-dnf  37656  poimirlem30  37790  poimirlem32  37792  ismblfin  37801  mbfposadd  37807  inixp  37868  elghomOLD  38027  keridl  38172  smprngopr  38192  sbcani  38248  inxpxrn  38542  dfcoss2  38615  cosscnv  38618  coss1cnvres  38619  coss2cnvepres  38620  1cossres  38631  dfcoels  38632  trressn  38647  br1cossinres  38649  br1cossinidres  38651  br1cossincnvepres  38652  br1cossxrnidres  38653  br1cossxrncnvepres  38654  cosscnvssid3  38678  coss0  38681  cossid  38682  trcoss  38684  eleccossin  38685  dfssr2  38691  br1cossxrncnvssrres  38700  refsymrels3  38762  refsymrel2  38763  refsymrel3  38764  elrefsymrels3  38766  dfeqvrel2  38786  dfeqvrel3  38787  redundeq1  38825  redundpbi1  38827  dfcomember3  38872  eqvreldmqs  38873  eqvreldmqs2  38874  dfeldisj3  38917  eldisjn0elb  38943  antisymrelres  38961  dfmembpart2  38968  prtlem10  39064  prter1  39078  lcvbr3  39222  isopos  39379  llnexatN  39720  snatpsubN  39949  pclclN  40090  pclfinN  40099  lhpocnel2  40218  cdlemk19w  41171  dih1dimatlem  41528  psspwb  42426  redvmptabs  42557  mzpclall  42911  mzpincl  42918  mzpindd  42930  2nn0ind  43129  dford4  43213  wopprc  43214  islmodfg  43253  ifpan123g  43642  ifpan23  43643  ifpnot23  43661  ifpdfxor  43670  ifpidg  43674  ifpid1g  43677  ifpim23g  43678  ifpim123g  43683  ifpim1g  43684  ifp1bi  43685  ifpimimb  43687  ifpororb  43688  ifpor123g  43691  ifpbibib  43693  rp-isfinite6  43701  alephiso2  43741  undmrnresiss  43787  cotrintab  43797  brtrclfv2  43910  dfxor4  43949  snhesn  43969  dffrege76  44122  uneqsn  44208  expandan  44471  ismnuprim  44477  nzin  44501  onfrALTlem5  44725  onfrALTlem4  44726  undif3VD  45064  onfrALTlem5VD  45067  onfrALTlem4VD  45068  dfac5prim  45173  wfaxpr  45181  brpermmodel  45186  permac8prim  45197  ndisj2  45238  rexabsle  45605  ellimcabssub0  45805  limsupre2mpt  45916  limsupre3  45919  limsupre3mpt  45920  limsupre3uz  45922  limsupreuz  45923  liminfreuz  45989  fourierdlem103  46395  fourierdlem104  46396  fourierdlem112  46404  smflim  46963  smflim2  46992  smflimsuplem1  47006  smflimsup  47014  cfsetsnfsetf1  47247  2reu8i  47301  ichan  47643  clnbgrsym  48026  dfnbgr6  48045  upgrimpthslem2  48096  isgrlim  48170  usgrexmpl2trifr  48225  pgnbgreunbgrlem5  48311  pgnbgreunbgr  48313  2zlidl  48428  islininds2  48672  zlmodzxzldeplem3  48690  2itscp  48969  reutruALT  48992  iinxp  49018  0funclem  49273  fucofulem2  49498  fuco2el  49499  catcinv  49586  2arwcatlem1  49782  alsi-no-surprise  49983