Theorem anbi12i 629

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.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	anbi1i 626	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	3	anbi2i 625	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
5	2, 4	bitri 278	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anbi12ci  630  ordi  1003  ordir  1004  orddi  1007  pm5.17  1009  xor  1012  cases2  1043  3anbi123i  1152  an6  1442  nanbi  1491  cadan  1611  nic-axALT  1676  19.43OLD  1884  sbbi  2313  sbbivOLD  2320  sbnf2  2366  eubii  2604  cbveuw  2625  cbveuALT  2628  2mo2  2668  2eu4  2675  sbabel  2950  neanior  3043  r19.26m  3104  rexeqbii  3250  reeanlem  3283  2ralor  3287  reu5  3340  reu2  3639  reu3  3641  2reu5a  3658  2reu5lem3  3671  2reu1  3803  eqss  3907  ss2abdv  3968  unss  4089  ralunb  4096  ssin  4135  undi  4179  indifdi  4188  indifdirOLD  4190  undif3  4195  inab  4203  difab  4204  reuss2  4217  reupick  4221  2reu4lem  4418  reuprg  4596  sstp  4724  tpss  4725  prneimg  4742  prnebg  4743  uniin  4824  intun  4870  intprOLD  4873  disjiun  5019  disjxiun  5029  brin  5084  brdif  5085  ssext  5315  pweqb  5317  opthg2  5339  copsex4g  5354  propeqop  5366  eqopab2bw  5405  eqopab2b  5409  pwin  5424  pofun  5460  wetrep  5517  elxp3  5587  soinxp  5602  weinxp  5605  csbxp  5619  relun  5653  inopab  5670  difopab  5671  inxp  5672  opelco2g  5707  cnvco  5725  dmin  5751  restidsing  5894  intasym  5947  asymref  5948  asymref2  5949  cnvdif  5974  xpnz  5988  difxp  5993  xpdifid  5997  xp11  6004  dfco2  6075  relssdmrn  6098  cnvpo  6116  cnvso  6117  xpco  6118  reu3op  6121  dffun4  6347  funun  6381  fun11  6409  fununi  6410  imadif  6419  fnres  6457  mptfnf  6466  fnopabg  6468  fun  6525  fin  6544  dff1o2  6607  brprcneu  6649  fvprc  6650  dffv2  6747  fsn  6888  f13dfv  7023  dff1o6  7024  isotr  7083  eqoprab2bw  7218  eqoprab2b  7219  fvmpopr2d  7306  porpss  7451  sucelon  7531  elxp6  7727  dfoprab3  7756  opiota  7761  poxp  7827  soxp  7828  suppvalbr  7839  brtpos2  7908  wfrlem5  7969  wfrfun  7975  tfrlem7  8029  dfer2  8300  eqer  8334  iiner  8379  uniinqs  8387  brecop  8400  eroveu  8402  erovlem  8403  mapval2  8454  ixpin  8505  boxriin  8522  brsdom  8550  xpcomco  8628  xpassen  8632  sbthlem9  8657  sbthlem10  8658  brsdom2  8663  ssenen  8713  unfiOLD  8818  dffi3  8928  dfsup2  8941  infcllem  8984  axinf2  9136  zfinf2  9138  oemapso  9178  scottexs  9349  scott0s  9350  kardex  9356  karden  9357  dfac5lem1  9583  dfac5lem3  9585  kmlem15  9624  enfin2i  9781  fin23lem34  9806  brdom7disj  9991  fpwwe2lem11  10101  fpwwe2lem12  10102  axgroth5  10284  grothprim  10294  addsrpr  10535  mulsrpr  10536  mulgt0sr  10565  addcnsr  10595  mulcnsr  10596  ltresr  10600  axcnre  10624  1re  10679  ssxr  10748  infrenegsup  11660  nnwos  12355  zmin  12384  xrnemnf  12553  xrnepnf  12554  xmullem  12698  xmulcom  12700  xmulneg1  12703  xmulf  12706  xrinfmss2  12745  elfzuzb  12950  fzass4  12994  seqof  13477  hashbclem  13860  hashfacen  13862  hashfacenOLD  13863  xpcogend  14381  trclublem  14402  rexanre  14754  caubnd  14766  o1lo1  14942  rpnnen2lem12  15626  lcmcllem  15992  lcmftp  16032  lcmfunsnlem2  16036  isprm3  16079  prmreclem2  16308  4sqlem12  16347  isffth2  17245  fucinv  17302  lublecllem  17664  oduglb  17815  odulub  17817  issubm  18034  issubmd  18037  0subm  18048  insubm  18049  sursubmefmnd  18127  injsubmefmnd  18128  smndex1mgm  18138  isnsg2  18375  cycsubm  18412  oppgid  18551  symgfixf1  18632  pmtrrn2  18655  lsmdisjr  18877  lsmhash  18898  gsumcom3  19166  dprd0  19221  issrg  19325  dvdsrtr  19473  isirred2  19522  lss1d  19803  lspsolvlem  19982  lbsextlem2  19999  cnfldfunALT  20179  unocv  20445  iunocv  20446  evlsval  20849  mpomatmul  21146  cpmidpmat  21573  tgval2  21656  fctop  21704  ppttop  21707  epttop  21709  cnnei  21982  2ndcctbss  22155  txuni2  22265  txbas  22267  ptbasin  22277  txdis1cn  22335  xkococnlem  22359  opnfbas  22542  fgcl  22578  fbasrn  22584  filuni  22585  cfinfil  22593  csdfil  22594  fin1aufil  22632  rnelfmlem  22652  fmfnfmlem3  22656  txflf  22706  xmeterval  23134  reconn  23529  iimulcl  23638  isclmp  23798  iscau3  23978  rrxmvallem  24104  minveclem3  24129  pmltpc  24150  ovolfcl  24166  ismbl  24226  dyaddisj  24296  iblre  24493  plyun0  24893  logfaclbnd  25905  lgslem3  25982  lgsdir2lem5  26012  tgjustf  26366  ishpg  26652  usgrexmpllem  27149  nb3grpr2  27272  vtxd0nedgb  27377  wlk1walk  27527  clwlkcompbp  27670  wwlknllvtx  27731  wwlksonvtx  27740  wspthnonp  27744  wwlksn0s  27746  wwlksnndef  27790  2wlkdlem8  27818  elwwlks2s3  27836  clwwlkf1  27933  clwwlknonccat  27980  clwwlknon2x  27987  3pthdlem1  28048  upgr4cycl4dv4e  28069  frgr2wwlk1  28213  frgrreg  28278  ajfval  28691  issh  29090  chcon2i  29346  chcon3i  29348  spanuni  29426  5oalem7  29542  3oalem3  29546  pjin2i  30075  pjin3i  30076  cvnbtwn4  30171  mdslj1i  30201  mdslj2i  30202  mdslmd1i  30211  chrelat4i  30255  chirredi  30276  cdj3i  30323  rmoun  30364  difrab2  30367  eqdif  30388  inpr0  30402  iuninc  30422  fcoinvbr  30469  suppss2f  30496  fmptdF  30517  disjdsct  30559  cnvoprabOLD  30579  f1od2  30580  hashxpe  30651  tosglblem  30778  mgcval  30791  pmtrprfv2  30883  ssmxidllem  31162  ccfldextdgrr  31263  ordtconnlem1  31395  esumpfinvalf  31563  esum2dlem  31579  measiuns  31704  eulerpartlemt0  31855  eulerpartlemr  31860  eulerpartlemn  31867  ballotlem2  31974  ballotlemodife  31983  bnj887  32264  bnj976  32277  bnj1385  32332  bnj153  32380  bnj543  32393  bnj607  32416  bnj882  32426  bnj916  32433  bnj983  32451  derangenlem  32649  pconnconn  32709  fmlaomn0  32868  fmla0disjsuc  32876  fmlasucdisj  32877  elmpst  33014  xpab  33195  dftr6  33233  dffr5  33236  dfpo2  33238  fundmpss  33256  elpotr  33273  poxp2  33345  xpord2pred  33347  xpord2ind  33349  xpord3pred  33353  soseq  33357  frrlem9  33392  fprlem1  33398  frrlem15  33403  nosupinfsep  33500  nocvxmin  33538  sltrec  33575  madebdaylemlrcut  33636  brtxp  33731  brpprod  33736  brsset  33740  idsset  33741  dfon3  33743  ellimits  33761  dffun10  33765  elfuns  33766  brcart  33783  brimg  33788  brapply  33789  brcap  33791  brsuccf  33792  funpartfun  33794  dfrecs2  33801  dfrdg4  33802  altopthc  33822  altopthd  33823  altopelaltxp  33827  outsideoftr  33980  trer  34054  neibastop1  34097  neifg  34109  df3nandALT1  34137  imnand2  34140  eliminable-abelab  34589  bj-eldiag2  34872  bj-imdiridlem  34880  bj-opabco  34883  bj-xpcossxp  34884  topdifinfeq  35047  relowlssretop  35060  relowlpssretop  35061  wl-cases2-dnf  35197  wl-dfreusb  35302  wl-dfreuv  35303  wl-dfrabv  35307  poimirlem30  35367  poimirlem32  35369  ismblfin  35378  mbfposadd  35384  inixp  35446  elghomOLD  35605  keridl  35750  smprngopr  35770  sbcani  35826  an2anr  35938  inxpxrn  36083  dfcoss2  36101  1cossres  36114  dfcoels  36115  br1cossinres  36127  br1cossinidres  36129  br1cossincnvepres  36130  br1cossxrnidres  36131  br1cossxrncnvepres  36132  cosscnvssid3  36156  coss0  36159  cossid  36160  trcoss  36162  eleccossin  36163  dfssr2  36179  br1cossxrncnvssrres  36188  refsymrels3  36242  refsymrel2  36243  refsymrel3  36244  elrefsymrels3  36246  dfeqvrel2  36265  dfeqvrel3  36266  redundeq1  36304  redundpbi1  36306  dfmember3  36348  eqvreldmqs  36349  dfeldisj3  36392  prtlem10  36441  prter1  36455  lcvbr3  36599  isopos  36756  llnexatN  37097  snatpsubN  37326  pclclN  37467  pclfinN  37476  lhpocnel2  37595  cdlemk19w  38548  dih1dimatlem  38905  psspwb  39708  mhphf  39790  mzpclall  40041  mzpincl  40048  mzpindd  40060  2nn0ind  40259  dford4  40343  wopprc  40344  islmodfg  40386  isdomn3  40521  ifpan123g  40540  ifpan23  40541  ifpnot23  40559  ifpdfxor  40568  ifpidg  40572  ifpid1g  40575  ifpim23g  40576  ifpim123g  40581  ifpim1g  40582  ifp1bi  40583  ifpimimb  40585  ifpororb  40586  ifpor123g  40589  ifpbibib  40591  rp-isfinite6  40599  alephiso2  40630  undmrnresiss  40677  cotrintab  40687  brtrclfv2  40801  dfxor4  40840  snhesn  40860  dffrege76  41013  uneqsn  41099  expandan  41369  ismnuprim  41375  nzin  41395  onfrALTlem5  41621  onfrALTlem4  41622  undif3VD  41961  onfrALTlem5VD  41964  onfrALTlem4VD  41965  ndisj2  42058  rexabsle  42422  ellimcabssub0  42625  limsupre2mpt  42738  limsupre3  42741  limsupre3mpt  42742  limsupre3uz  42744  limsupreuz  42745  liminfreuz  42811  fourierdlem103  43217  fourierdlem104  43218  fourierdlem112  43226  smflim  43776  smflim2  43803  smflimsuplem1  43817  smflimsup  43825  2reu8i  44037  ichan  44340  issubmgm  44776  rabsubmgmd  44778  2zlidl  44925  mndpsuppss  45140  islininds2  45258  zlmodzxzldeplem3  45276  2itscp  45560  alsi-no-surprise  45715