Theorem anbi12i 627

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  anbi12ci  628  an2anr  635  ordi  1004  ordir  1005  orddi  1008  pm5.17  1010  xor  1013  cases2  1046  3anbi123i  1155  an6  1445  nanbi  1498  cadan  1610  nic-axALT  1676  19.43OLD  1886  sbbi  2304  aaan  2327  sbnf2  2354  eubii  2578  cbveuvw  2599  cbveuw  2600  cbveuALT  2603  2mo2  2642  2eu4  2649  sbabel  2937  sbabelOLD  2938  neanior  3034  r19.26m  3109  reeanlem  3214  2ralorOLD  3218  rexeqbii  3314  reu5  3353  cbvreuw  3381  reu2  3686  reu3  3688  2reu5a  3705  2reu5lem3  3718  2reu1  3856  eqss  3962  ss2abdv  4025  unss  4149  ralunb  4156  ssin  4195  undi  4239  indifdi  4248  indifdirOLD  4250  undif3  4255  inab  4264  difab  4265  reuss2  4280  reupick  4283  2reu4lem  4488  reuprg  4669  sstp  4799  tpss  4800  prneimg  4817  prnebg  4818  uniin  4897  intun  4946  intprOLD  4949  disjiun  5097  disjxiun  5107  brin  5162  brdif  5163  ssext  5416  pweqb  5418  opthg2  5441  copsex4g  5457  propeqop  5469  eqopab2bw  5510  eqopab2b  5514  pwin  5532  pofun  5568  dffr6  5596  wetrep  5631  elxp3  5703  soinxp  5718  weinxp  5721  csbxp  5736  relun  5772  inopab  5790  difopab  5791  difopabOLD  5792  inxp  5793  opelco2g  5828  cnvco  5846  dmin  5872  restidsing  6011  intasym  6074  asymref  6075  asymref2  6076  cnvdif  6101  xpnz  6116  difxp  6121  xpdifid  6125  xp11  6132  dfco2  6202  relssdmrnOLD  6226  cnvpo  6244  cnvso  6245  xpco  6246  reu3op  6249  dfpo2  6253  dffun4  6517  funun  6552  fun11  6580  fununi  6581  imadif  6590  fnres  6633  mptfnf  6641  fnopabg  6643  fun  6709  fin  6727  dff1o2  6794  brprcneu  6837  brprcneuALT  6838  dffv2  6941  fsn  7086  f13dfv  7225  dff1o6  7226  isotr  7286  eqoprab2bw  7432  eqoprab2b  7433  fvmpopr2d  7521  porpss  7669  epweon  7714  onsucb  7757  elxp6  7960  dfoprab3  7991  opiota  7996  poxp  8065  soxp  8066  poxp2  8080  xpord2pred  8082  xpord2indlem  8084  xpord3pred  8089  xpord3inddlem  8091  soseq  8096  suppvalbr  8101  brtpos2  8168  frrlem9  8230  fprlem1  8236  wfrlem5OLD  8264  wfrfunOLD  8270  tfrlem7  8334  dfer2  8656  eqer  8690  iiner  8735  uniinqs  8743  brecop  8756  eroveu  8758  erovlem  8759  fsetexb  8809  mapval2  8817  ixpin  8868  boxriin  8885  brsdom  8922  xpcomco  9013  xpassen  9017  sbthlem9  9042  sbthlem10  9043  brsdom2  9048  ssenen  9102  sbthfilem  9152  unfiOLD  9264  dffi3  9376  dfsup2  9389  infcllem  9432  axinf2  9585  zfinf2  9587  oemapso  9627  ttrcltr  9661  frrlem15  9702  scottexs  9832  scott0s  9833  kardex  9839  karden  9840  dfac5lem1  10068  dfac5lem3  10070  kmlem15  10109  enfin2i  10266  fin23lem34  10291  brdom7disj  10476  fpwwe2lem11  10586  fpwwe2lem12  10587  axgroth5  10769  grothprim  10779  addsrpr  11020  mulsrpr  11021  mulgt0sr  11050  addcnsr  11080  mulcnsr  11081  ltresr  11085  axcnre  11109  1re  11164  ssxr  11233  infrenegsup  12147  nnwos  12849  zmin  12878  xrnemnf  13047  xrnepnf  13048  xmullem  13193  xmulcom  13195  xmulneg1  13198  xmulf  13201  xrinfmss2  13240  elfzuzb  13445  fzass4  13489  seqof  13975  hashbclem  14361  hashfacen  14363  hashfacenOLD  14364  xpcogend  14871  trclublem  14892  rexanre  15243  caubnd  15255  o1lo1  15431  rpnnen2lem12  16118  lcmcllem  16483  lcmftp  16523  lcmfunsnlem2  16527  isprm3  16570  prmreclem2  16800  4sqlem12  16839  catcone0  17581  isffth2  17817  fucinv  17876  lublecllem  18263  odulub  18310  oduglb  18312  issubm  18628  issubmd  18631  0subm  18642  insubm  18643  sursubmefmnd  18720  injsubmefmnd  18721  smndex1mgm  18731  isnsg2  18972  cycsubm  19009  oppgid  19151  symgfixf1  19233  pmtrrn2  19256  lsmdisjr  19480  lsmhash  19501  gsumcom3  19769  dprd0  19824  issrg  19933  dvdsrtr  20095  isirred2  20146  lss1d  20481  lspsolvlem  20662  lbsextlem2  20679  cnfldfun  20845  unocv  21121  iunocv  21122  evlsval  21533  mpomatmul  21832  cpmidpmat  22259  tgval2  22343  fctop  22391  ppttop  22394  epttop  22396  cnnei  22670  2ndcctbss  22843  txuni2  22953  txbas  22955  ptbasin  22965  txdis1cn  23023  xkococnlem  23047  opnfbas  23230  fgcl  23266  fbasrn  23272  filuni  23273  cfinfil  23281  csdfil  23282  fin1aufil  23320  rnelfmlem  23340  fmfnfmlem3  23344  txflf  23394  xmeterval  23822  reconn  24228  iimulcl  24337  isclmp  24497  iscau3  24679  rrxmvallem  24805  minveclem3  24830  pmltpc  24851  ovolfcl  24867  ismbl  24927  dyaddisj  24997  iblre  25195  plyun0  25595  logfaclbnd  26607  lgslem3  26684  lgsdir2lem5  26714  nosupinfsep  27117  nocvxmin  27161  sltrec  27202  madebdaylemlrcut  27271  addsproplem2  27325  addsunif  27353  negsproplem2  27370  negsid  27382  mulsproplem10  27431  tgjustf  27478  ishpg  27764  usgrexmpllem  28271  nb3grpr2  28394  vtxd0nedgb  28499  wlk1walk  28650  clwlkcompbp  28793  wwlknllvtx  28854  wwlksonvtx  28863  wspthnonp  28867  wwlksn0s  28869  wwlksnndef  28913  2wlkdlem8  28941  elwwlks2s3  28959  clwwlkf1  29056  clwwlknonccat  29103  clwwlknon2x  29110  3pthdlem1  29171  upgr4cycl4dv4e  29192  frgr2wwlk1  29336  frgrreg  29401  ajfval  29814  issh  30213  chcon2i  30469  chcon3i  30471  spanuni  30549  5oalem7  30665  3oalem3  30669  pjin2i  31198  pjin3i  31199  cvnbtwn4  31294  mdslj1i  31324  mdslj2i  31325  mdslmd1i  31334  chrelat4i  31378  chirredi  31399  cdj3i  31446  rmoun  31486  difrab2  31490  eqdif  31510  inpr0  31523  iuninc  31546  fcoinvbr  31593  suppss2f  31620  fmptdF  31639  disjdsct  31684  cnvoprabOLD  31705  f1od2  31706  hashxpe  31779  tosglblem  31904  mgcval  31917  pmtrprfv2  32009  ssmxidllem  32314  ccfldextdgrr  32443  ordtconnlem1  32594  esumpfinvalf  32764  esum2dlem  32780  measiuns  32905  eulerpartlemt0  33058  eulerpartlemr  33063  eulerpartlemn  33070  ballotlem2  33177  ballotlemodife  33186  bnj887  33466  bnj976  33478  bnj1385  33533  bnj153  33581  bnj543  33594  bnj607  33617  bnj882  33627  bnj916  33634  bnj983  33652  derangenlem  33852  pconnconn  33912  fmlaomn0  34071  fmla0disjsuc  34079  fmlasucdisj  34080  elmpst  34217  xpab  34384  dftr6  34410  dffr5  34413  fundmpss  34427  elpotr  34442  brtxp  34541  brpprod  34546  brsset  34550  idsset  34551  dfon3  34553  ellimits  34571  dffun10  34575  elfuns  34576  brcart  34593  brimg  34598  brapply  34599  brcap  34601  brsuccf  34602  funpartfun  34604  dfrecs2  34611  dfrdg4  34612  altopthc  34632  altopthd  34633  altopelaltxp  34637  outsideoftr  34790  trer  34864  neibastop1  34907  neifg  34919  df3nandALT1  34947  imnand2  34950  eliminable-abelab  35412  bj-eldiag2  35721  bj-imdiridlem  35729  bj-opabco  35732  bj-xpcossxp  35733  topdifinfeq  35894  relowlssretop  35907  relowlpssretop  35908  wl-cases2-dnf  36044  poimirlem30  36181  poimirlem32  36183  ismblfin  36192  mbfposadd  36198  inixp  36260  elghomOLD  36419  keridl  36564  smprngopr  36584  sbcani  36640  inxpxrn  36930  dfcoss2  36948  cosscnv  36951  coss1cnvres  36952  coss2cnvepres  36953  1cossres  36964  dfcoels  36965  trressn  36980  br1cossinres  36982  br1cossinidres  36984  br1cossincnvepres  36985  br1cossxrnidres  36986  br1cossxrncnvepres  36987  cosscnvssid3  37011  coss0  37014  cossid  37015  trcoss  37017  eleccossin  37018  dfssr2  37034  br1cossxrncnvssrres  37043  refsymrels3  37101  refsymrel2  37102  refsymrel3  37103  elrefsymrels3  37105  dfeqvrel2  37125  dfeqvrel3  37126  redundeq1  37164  redundpbi1  37166  dfcomember3  37209  eqvreldmqs  37210  eqvreldmqs2  37211  dfeldisj3  37254  eldisjn0elb  37280  antisymrelres  37298  dfmembpart2  37305  prtlem10  37400  prter1  37414  lcvbr3  37558  isopos  37715  llnexatN  38057  snatpsubN  38286  pclclN  38427  pclfinN  38436  lhpocnel2  38555  cdlemk19w  39508  dih1dimatlem  39865  psspwb  40722  mhphf  40829  mzpclall  41108  mzpincl  41115  mzpindd  41127  2nn0ind  41327  dford4  41411  wopprc  41412  islmodfg  41454  isdomn3  41589  ifpan123g  41853  ifpan23  41854  ifpnot23  41872  ifpdfxor  41881  ifpidg  41885  ifpid1g  41888  ifpim23g  41889  ifpim123g  41894  ifpim1g  41895  ifp1bi  41896  ifpimimb  41898  ifpororb  41899  ifpor123g  41902  ifpbibib  41904  rp-isfinite6  41912  alephiso2  41952  undmrnresiss  41998  cotrintab  42008  brtrclfv2  42121  dfxor4  42160  snhesn  42180  dffrege76  42333  uneqsn  42419  expandan  42690  ismnuprim  42696  nzin  42720  onfrALTlem5  42946  onfrALTlem4  42947  undif3VD  43286  onfrALTlem5VD  43289  onfrALTlem4VD  43290  ndisj2  43381  rexabsle  43774  ellimcabssub0  43978  limsupre2mpt  44091  limsupre3  44094  limsupre3mpt  44095  limsupre3uz  44097  limsupreuz  44098  liminfreuz  44164  fourierdlem103  44570  fourierdlem104  44571  fourierdlem112  44579  smflim  45138  smflim2  45167  smflimsuplem1  45181  smflimsup  45189  cfsetsnfsetf1  45413  2reu8i  45465  ichan  45767  issubmgm  46203  rabsubmgmd  46205  2zlidl  46352  mndpsuppss  46567  islininds2  46685  zlmodzxzldeplem3  46703  2itscp  46987  reutruALT  47011  alsi-no-surprise  47363