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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anbi12ci  629  an2anr  636  ordi  1005  ordir  1006  orddi  1009  pm5.17  1011  xor  1014  cases2  1047  3anbi123i  1156  an6  1446  nanbi  1499  cadan  1611  nic-axALT  1677  19.43OLD  1887  sbbi  2305  aaan  2328  sbnf2  2355  eubii  2580  cbveuvw  2601  cbveuw  2602  cbveuALT  2605  2mo2  2644  2eu4  2651  sbabel  2939  sbabelOLD  2940  neanior  3036  r19.26m  3111  reeanlem  3226  2ralorOLD  3230  rexeqbii  3340  reu5  3379  cbvreuw  3407  cgsex4g  3521  reu2  3722  reu3  3724  2reu5a  3741  2reu5lem3  3754  2reu1  3892  eqss  3998  ss2abdv  4061  unss  4185  ralunb  4192  ssin  4231  undi  4275  indifdi  4284  indifdirOLD  4286  undif3  4291  inab  4300  difab  4301  reuss2  4316  reupick  4319  2reu4lem  4526  reuprg  4708  sstp  4838  tpss  4839  prneimg  4856  prnebg  4857  uniin  4936  intun  4985  intprOLD  4988  disjiun  5136  disjxiun  5146  brin  5201  brdif  5202  ssext  5455  pweqb  5457  opthg2  5480  copsex4g  5496  propeqop  5508  eqopab2bw  5549  eqopab2b  5553  pwin  5571  pofun  5607  dffr6  5635  wetrep  5670  elxp3  5743  soinxp  5758  weinxp  5761  csbxp  5776  relun  5812  inopab  5830  difopab  5831  difopabOLD  5832  inxp  5833  opelco2g  5868  cnvco  5886  dmin  5912  restidsing  6053  intasym  6117  asymref  6118  asymref2  6119  cnvdif  6144  xpnz  6159  difxp  6164  xpdifid  6168  xp11  6175  dfco2  6245  relssdmrnOLD  6269  cnvpo  6287  cnvso  6288  xpco  6289  reu3op  6292  dfpo2  6296  dffun4  6560  funun  6595  fun11  6623  fununi  6624  imadif  6633  fnres  6678  mptfnf  6686  fnopabg  6688  fun  6754  fin  6772  dff1o2  6839  brprcneu  6882  brprcneuALT  6883  dffv2  6987  fsn  7133  f13dfv  7272  dff1o6  7273  isotr  7333  eqoprab2bw  7479  eqoprab2b  7480  fvmpopr2d  7569  porpss  7717  epweon  7762  onsucb  7805  elxp6  8009  dfoprab3  8040  opiota  8045  poxp  8114  soxp  8115  poxp2  8129  xpord2pred  8131  xpord2indlem  8133  xpord3pred  8138  xpord3inddlem  8140  soseq  8145  suppvalbr  8150  brtpos2  8217  frrlem9  8279  fprlem1  8285  wfrlem5OLD  8313  wfrfunOLD  8319  tfrlem7  8383  dfer2  8704  eqer  8738  iiner  8783  uniinqs  8791  brecop  8804  eroveu  8806  erovlem  8807  fsetexb  8858  mapval2  8866  ixpin  8917  boxriin  8934  brsdom  8971  xpcomco  9062  xpassen  9066  sbthlem9  9091  sbthlem10  9092  brsdom2  9097  ssenen  9151  sbthfilem  9201  unfiOLD  9313  dffi3  9426  dfsup2  9439  infcllem  9482  axinf2  9635  zfinf2  9637  oemapso  9677  ttrcltr  9711  frrlem15  9752  scottexs  9882  scott0s  9883  kardex  9889  karden  9890  dfac5lem1  10118  dfac5lem3  10120  kmlem15  10159  enfin2i  10316  fin23lem34  10341  brdom7disj  10526  fpwwe2lem11  10636  fpwwe2lem12  10637  axgroth5  10819  grothprim  10829  addsrpr  11070  mulsrpr  11071  mulgt0sr  11100  addcnsr  11130  mulcnsr  11131  ltresr  11135  axcnre  11159  1re  11214  ssxr  11283  infrenegsup  12197  nnwos  12899  zmin  12928  xrnemnf  13097  xrnepnf  13098  xmullem  13243  xmulcom  13245  xmulneg1  13248  xmulf  13251  xrinfmss2  13290  elfzuzb  13495  fzass4  13539  seqof  14025  hashbclem  14411  hashfacen  14413  hashfacenOLD  14414  xpcogend  14921  trclublem  14942  rexanre  15293  caubnd  15305  o1lo1  15481  rpnnen2lem12  16168  lcmcllem  16533  lcmftp  16573  lcmfunsnlem2  16577  isprm3  16620  prmreclem2  16850  4sqlem12  16889  catcone0  17631  isffth2  17867  fucinv  17926  lublecllem  18313  odulub  18360  oduglb  18362  issubm  18684  issubmd  18687  0subm  18698  insubm  18699  sursubmefmnd  18777  injsubmefmnd  18778  smndex1mgm  18788  isnsg2  19036  cycsubm  19079  oppgid  19223  symgfixf1  19305  pmtrrn2  19328  lsmdisjr  19552  lsmhash  19573  gsumcom3  19846  dprd0  19901  issrg  20011  dvdsrtr  20182  isirred2  20235  lss1d  20574  lspsolvlem  20755  lbsextlem2  20772  cnfldfun  20956  unocv  21233  iunocv  21234  evlsval  21649  mpomatmul  21948  cpmidpmat  22375  tgval2  22459  fctop  22507  ppttop  22510  epttop  22512  cnnei  22786  2ndcctbss  22959  txuni2  23069  txbas  23071  ptbasin  23081  txdis1cn  23139  xkococnlem  23163  opnfbas  23346  fgcl  23382  fbasrn  23388  filuni  23389  cfinfil  23397  csdfil  23398  fin1aufil  23436  rnelfmlem  23456  fmfnfmlem3  23460  txflf  23510  xmeterval  23938  reconn  24344  iimulcl  24453  isclmp  24613  iscau3  24795  rrxmvallem  24921  minveclem3  24946  pmltpc  24967  ovolfcl  24983  ismbl  25043  dyaddisj  25113  iblre  25311  plyun0  25711  logfaclbnd  26725  lgslem3  26802  lgsdir2lem5  26832  nosupinfsep  27235  nocvxmin  27280  sltrec  27322  madebdaylemlrcut  27394  addsproplem2  27456  addsuniflem  27487  negsproplem2  27506  negsid  27518  mulsproplem5  27579  mulsproplem6  27580  mulsproplem7  27581  mulsproplem8  27582  mulsproplem9  27583  mulsuniflem  27607  precsexlem9  27664  precsexlem10  27665  tgjustf  27755  ishpg  28041  usgrexmpllem  28548  nb3grpr2  28671  vtxd0nedgb  28776  wlk1walk  28927  clwlkcompbp  29070  wwlknllvtx  29131  wwlksonvtx  29140  wspthnonp  29144  wwlksn0s  29146  wwlksnndef  29190  2wlkdlem8  29218  elwwlks2s3  29236  clwwlkf1  29333  clwwlknonccat  29380  clwwlknon2x  29387  3pthdlem1  29448  upgr4cycl4dv4e  29469  frgr2wwlk1  29613  frgrreg  29678  ajfval  30093  issh  30492  chcon2i  30748  chcon3i  30750  spanuni  30828  5oalem7  30944  3oalem3  30948  pjin2i  31477  pjin3i  31478  cvnbtwn4  31573  mdslj1i  31603  mdslj2i  31604  mdslmd1i  31613  chrelat4i  31657  chirredi  31678  cdj3i  31725  rmoun  31765  difrab2  31769  eqdif  31788  inpr0  31800  iuninc  31823  fcoinvbr  31867  suppss2f  31894  fmptdF  31912  disjdsct  31955  cnvoprabOLD  31976  f1od2  31977  hashxpe  32050  tosglblem  32175  mgcval  32188  pmtrprfv2  32280  ssmxidllem  32620  ccfldextdgrr  32777  ordtconnlem1  32935  esumpfinvalf  33105  esum2dlem  33121  measiuns  33246  eulerpartlemt0  33399  eulerpartlemr  33404  eulerpartlemn  33411  ballotlem2  33518  ballotlemodife  33527  bnj887  33807  bnj976  33819  bnj1385  33874  bnj153  33922  bnj543  33935  bnj607  33958  bnj882  33968  bnj916  33975  bnj983  33993  derangenlem  34193  pconnconn  34253  fmlaomn0  34412  fmla0disjsuc  34420  fmlasucdisj  34421  elmpst  34558  xpab  34726  dftr6  34752  dffr5  34755  fundmpss  34769  elpotr  34784  brtxp  34883  brpprod  34888  brsset  34892  idsset  34893  dfon3  34895  ellimits  34913  dffun10  34917  elfuns  34918  brcart  34935  brimg  34940  brapply  34941  brcap  34943  brsuccf  34944  funpartfun  34946  dfrecs2  34953  dfrdg4  34954  altopthc  34974  altopthd  34975  altopelaltxp  34979  outsideoftr  35132  gg-cnfldfun  35228  trer  35249  neibastop1  35292  neifg  35304  df3nandALT1  35332  imnand2  35335  eliminable-abelab  35797  bj-eldiag2  36106  bj-imdiridlem  36114  bj-opabco  36117  bj-xpcossxp  36118  topdifinfeq  36279  relowlssretop  36292  relowlpssretop  36293  wl-cases2-dnf  36429  poimirlem30  36566  poimirlem32  36568  ismblfin  36577  mbfposadd  36583  inixp  36644  elghomOLD  36803  keridl  36948  smprngopr  36968  sbcani  37024  inxpxrn  37313  dfcoss2  37331  cosscnv  37334  coss1cnvres  37335  coss2cnvepres  37336  1cossres  37347  dfcoels  37348  trressn  37363  br1cossinres  37365  br1cossinidres  37367  br1cossincnvepres  37368  br1cossxrnidres  37369  br1cossxrncnvepres  37370  cosscnvssid3  37394  coss0  37397  cossid  37398  trcoss  37400  eleccossin  37401  dfssr2  37417  br1cossxrncnvssrres  37426  refsymrels3  37484  refsymrel2  37485  refsymrel3  37486  elrefsymrels3  37488  dfeqvrel2  37508  dfeqvrel3  37509  redundeq1  37547  redundpbi1  37549  dfcomember3  37592  eqvreldmqs  37593  eqvreldmqs2  37594  dfeldisj3  37637  eldisjn0elb  37663  antisymrelres  37681  dfmembpart2  37688  prtlem10  37783  prter1  37797  lcvbr3  37941  isopos  38098  llnexatN  38440  snatpsubN  38669  pclclN  38810  pclfinN  38819  lhpocnel2  38938  cdlemk19w  39891  dih1dimatlem  40248  psspwb  41094  mzpclall  41513  mzpincl  41520  mzpindd  41532  2nn0ind  41732  dford4  41816  wopprc  41817  islmodfg  41859  isdomn3  41994  ifpan123g  42258  ifpan23  42259  ifpnot23  42277  ifpdfxor  42286  ifpidg  42290  ifpid1g  42293  ifpim23g  42294  ifpim123g  42299  ifpim1g  42300  ifp1bi  42301  ifpimimb  42303  ifpororb  42304  ifpor123g  42307  ifpbibib  42309  rp-isfinite6  42317  alephiso2  42357  undmrnresiss  42403  cotrintab  42413  brtrclfv2  42526  dfxor4  42565  snhesn  42585  dffrege76  42738  uneqsn  42824  expandan  43095  ismnuprim  43101  nzin  43125  onfrALTlem5  43351  onfrALTlem4  43352  undif3VD  43691  onfrALTlem5VD  43694  onfrALTlem4VD  43695  ndisj2  43786  rexabsle  44177  ellimcabssub0  44381  limsupre2mpt  44494  limsupre3  44497  limsupre3mpt  44498  limsupre3uz  44500  limsupreuz  44501  liminfreuz  44567  fourierdlem103  44973  fourierdlem104  44974  fourierdlem112  44982  smflim  45541  smflim2  45570  smflimsuplem1  45584  smflimsup  45592  cfsetsnfsetf1  45817  2reu8i  45869  ichan  46171  issubmgm  46607  rabsubmgmd  46609  2zlidl  46880  mndpsuppss  47095  islininds2  47213  zlmodzxzldeplem3  47231  2itscp  47515  reutruALT  47539  alsi-no-surprise  47891