Theorem anbi12i 614

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 612	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
3		anbi12.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	3	anbi2i 611	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))
5	2, 4	bitri 266	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

Syntax hints:   ↔ wb 197   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  anbi12ci  615  ordi  1019  ordir  1020  orddi  1023  pm5.17  1026  xor  1029  cases2  1061  3anbi123i  1187  an6  1562  nanbi  1608  cadan  1703  nic-axALT  1754  19.43OLD  1973  sbequ8  2064  sbbi  2559  sbnf2  2600  2mo2  2711  2eu4  2717  sbabel  2973  neanior  3066  rexeqbii  3238  r19.26m  3251  reean  3290  2ralor  3293  reu5  3344  reu2  3586  reu3  3588  2reu5lem3  3607  eqss  3807  unss  3980  ralunb  3987  ssin  4025  undi  4070  indifdir  4079  undif3  4084  inab  4090  difab  4091  reuss2  4102  reupick  4106  ssdifsnOLD  4504  sstp  4549  tpss  4550  prneimg  4568  prnebg  4569  uniin  4645  intun  4694  intpr  4695  disjiun  4825  disjxiun  4834  brin  4889  brdif  4890  ssext  5107  pweqb  5109  opthg2  5131  copsex4g  5142  propeqop  5156  eqopab2b  5194  pwin  5207  pofun  5242  wetrep  5298  elxp3  5363  soinxp  5379  weinxp  5382  csbxp  5396  relun  5430  inopab  5448  difopab  5449  inxp  5450  opelco2g  5485  cnvco  5503  dmin  5527  restidsing  5664  intasym  5716  asymref  5717  asymref2  5718  cnvdif  5744  xpnz  5758  difxp  5763  xpdifid  5767  xp11  5774  dfco2  5842  relssdmrn  5864  cnvpo  5881  cnvso  5882  xpco  5883  dffun4  6107  funun  6140  fun11  6168  fununi  6169  imadif  6178  fnres  6212  mptfnf  6220  fnopabg  6222  fun  6275  fin  6294  dff1o2  6352  brprcneu  6394  dffv2  6486  fsn  6619  f13dfv  6748  dff1o6  6749  isotr  6804  eqoprab2b  6937  porpss  7165  sucelon  7241  elxp6  7426  dfoprab3  7450  opiota  7455  fsplit  7510  poxp  7517  soxp  7518  suppvalbr  7527  brtpos2  7587  wfrlem5  7649  wfrfun  7655  tfrlem7  7709  dfer2  7974  eqer  8008  iiner  8048  uniinqs  8056  brecop  8069  eroveu  8072  erovlem  8073  mapval2  8116  ixpin  8164  boxriin  8181  brsdom  8209  xpcomco  8283  xpassen  8287  sbthlem9  8311  sbthlem10  8312  brsdom2  8317  ssenen  8367  unfi  8460  dffi3  8570  dfsup2  8583  infcllem  8626  axinf2  8778  zfinf2  8780  oemapso  8820  scottexs  8991  scott0s  8992  kardex  8998  karden  8999  dfac5lem1  9223  dfac5lem3  9225  kmlem15  9265  enfin2i  9422  fin23lem34  9447  brdom7disj  9632  fpwwe2lem12  9742  fpwwe2lem13  9743  axgroth5  9925  grothprim  9935  addsrpr  10175  mulsrpr  10176  mulgt0sr  10205  addcnsr  10235  mulcnsr  10236  ltresr  10240  axcnre  10264  1re  10319  ssxr  10386  infrenegsup  11285  nnwos  11968  zmin  11997  xrnemnf  12161  xrnepnf  12162  xmullem  12306  xmulcom  12308  xmulneg1  12311  xmulf  12314  xrinfmss2  12353  elfzuzb  12553  fzass4  12596  seqof  13075  hashbclem  13447  hashfacen  13449  xpcogend  13932  trclublem  13953  rexanre  14303  caubnd  14315  o1lo1  14485  rpnnen2lem12  15168  lcmcllem  15522  lcmftp  15562  lcmfunsnlem2  15566  isprm3  15608  prmreclem2  15832  4sqlem12  15871  isffth2  16774  fucinv  16831  lublecllem  17187  oduglb  17338  odulub  17340  issubm  17546  issubmd  17548  isnsg2  17820  oppgid  17981  symgfixf1  18052  pmtrrn2  18075  lsmdisjr  18292  lsmhash  18313  dprd0  18626  issrg  18703  dvdsrtr  18848  isirred2  18897  lss1d  19164  lspsolvlem  19344  lbsextlem2  19362  evlsval  19721  cnfldfunALT  19961  unocv  20228  iunocv  20229  gsumcom3  20409  mpt2matmul  20457  cpmidpmat  20885  tgval2  20968  fctop  21016  ppttop  21019  epttop  21021  cnnei  21294  2ndcctbss  21466  txuni2  21576  txbas  21578  ptbasin  21588  txdis1cn  21646  xkococnlem  21670  opnfbas  21853  fgcl  21889  fbasrn  21895  filuni  21896  cfinfil  21904  csdfil  21905  fin1aufil  21943  rnelfmlem  21963  fmfnfmlem3  21967  txflf  22017  xmeterval  22444  reconn  22838  iimulcl  22943  isclmp  23103  iscau3  23282  rrxmvallem  23393  minveclem3  23406  pmltpc  23425  ovolfcl  23441  ismbl  23501  dyaddisj  23571  iblre  23768  plyun0  24161  logfaclbnd  25155  lgslem3  25232  lgsdir2lem5  25262  ishpg  25859  usgrexmpllem  26362  nb3grpr2  26495  vtxd0nedgb  26606  wlk1walk  26757  clwlkcompbp  26900  wwlknllvtx  26962  wwlksonvtx  26972  wspthnonp  26980  wwlksn0s  26982  wlknwwlksninjOLD  27010  wlkwwlkinjOLD  27018  wwlksnndef  27036  wwlksnfi  27037  2wlkdlem8  27067  elwwlks2s3  27085  clwwlkf1  27192  clwwlknonccat  27258  clwwlknon2x  27265  3pthdlem1  27331  upgr4cycl4dv4e  27352  frgr2wwlk1  27498  frgrreg  27576  ajfval  27986  issh  28387  chcon2i  28645  chcon3i  28647  spanuni  28725  5oalem7  28841  3oalem3  28845  pjin2i  29374  pjin3i  29375  cvnbtwn4  29470  mdslj1i  29500  mdslj2i  29501  mdslmd1i  29510  chrelat4i  29554  chirredi  29575  cdj3i  29622  difrab2  29658  iuninc  29698  fcoinvbr  29738  suppss2f  29760  fmptdF  29777  disjdsct  29801  cnvoprabOLD  29819  f1od2  29820  tosglblem  29988  pmtrprfv2  30167  ordtconnlem1  30289  esumpfinvalf  30457  esum2dlem  30473  measiuns  30599  eulerpartlemt0  30750  eulerpartlemr  30755  eulerpartlemn  30762  ballotlem2  30869  ballotlemodife  30878  bnj887  31152  bnj976  31165  bnj1385  31220  bnj153  31267  bnj543  31280  bnj607  31303  bnj882  31313  bnj916  31320  bnj983  31338  derangenlem  31470  pconnconn  31530  elmpst  31750  dftr6  31956  dffr5  31959  dfpo2  31961  fundmpss  31980  elpotr  32000  soseq  32069  frrlem5  32099  frrlem5c  32101  nocvxmin  32209  sltrec  32239  brtxp  32302  brpprod  32307  brsset  32311  idsset  32312  dfon3  32314  ellimits  32332  dffun10  32336  elfuns  32337  brcart  32354  brimg  32359  brapply  32360  brcap  32362  brsuccf  32363  funpartfun  32365  dfrecs2  32372  dfrdg4  32373  altopthc  32393  altopthd  32394  altopelaltxp  32398  outsideoftr  32551  trer  32625  gtinfOLD  32629  neibastop1  32669  neifg  32681  df3nandALT1  32709  imnand2  32712  bj-eldiag2  33403  topdifinfeq  33508  relowlssretop  33521  relowlpssretop  33522  wl-cases2-dnf  33605  poimirlem30  33746  poimirlem32  33748  ismblfin  33757  mbfposadd  33763  inixp  33829  elghomOLD  33991  keridl  34136  smprngopr  34156  sbcani  34215  an2anr  34313  inxpxrn  34460  dfcoss2  34478  1cossres  34491  dfcoels  34492  br1cossinres  34504  br1cossinidres  34506  br1cossincnvepres  34507  br1cossxrnidres  34508  br1cossxrncnvepres  34509  cosscnvssid3  34533  coss0  34536  cossid  34537  trcoss  34539  eleccossin  34540  dfssr2  34556  br1cossxrncnvssrres  34565  refsymrels3  34619  refsymrel2  34620  refsymrel3  34621  elrefsymrels3  34623  prtlem10  34638  prter1  34652  lcvbr3  34797  isopos  34954  llnexatN  35295  snatpsubN  35524  pclclN  35665  pclfinN  35674  lhpocnel2  35793  cdlemk19w  36747  dih1dimatlem  37104  psspwb  37746  mzpclall  37786  mzpincl  37793  mzpindd  37805  2nn0ind  38005  dford4  38091  wopprc  38092  islmodfg  38134  isdomn3  38277  ifpan123g  38297  ifpan23  38298  ifpdfbi  38312  ifpnot23  38317  ifpdfxor  38326  ifpidg  38330  ifpid1g  38333  ifpim23g  38334  ifpim123g  38339  ifpim1g  38340  ifp1bi  38341  ifpimimb  38343  ifpororb  38344  ifpor123g  38347  ifpbibib  38349  rp-isfinite6  38358  undmrnresiss  38404  cotrintab  38415  brtrclfv2  38513  dfxor4  38552  snhesn  38574  dffrege76  38727  uneqsn  38815  nzin  39011  onfrALTlem5  39249  onfrALTlem4  39250  undif3VD  39606  onfrALTlem5VD  39609  onfrALTlem4VD  39610  ndisj2  39705  rexabsle  40119  ellimcabssub0  40323  limsupre2mpt  40436  limsupre3  40439  limsupre3mpt  40440  limsupre3uz  40442  limsupreuz  40443  liminfreuz  40509  fourierdlem103  40899  fourierdlem104  40900  fourierdlem112  40908  smflim  41461  smflim2  41488  smflimsuplem1  41502  smflimsup  41510  2reu5a  41683  2reu1  41692  2reu4a  41695  issubmgm  42351  rabsubmgmd  42353  2zlidl  42496  mndpsuppss  42714  islininds2  42835  zlmodzxzldeplem3  42853  alsi-no-surprise  43107