Theorem anbi12i 639

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 634	. 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜃))
3		anbi12.1	. 2 ⊢ (𝜑 ↔ 𝜓)
4	2, 3	bianbi 638	1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 401

This theorem is referenced by:  anbi12ci  640  an2anr  647  ordi  1021  ordir  1022  orddi  1025  pm5.17  1027  xor  1030  cases2  1061  3anbi123i  1171  an6  1471  nanbi  1527  cadan  1636  nic-axALT  1701  19.43OLD  1910  sbbi  2348  aaan  2371  sbnf2  2396  cbveuvw  2639  cbveuw  2640  cbveuALT  2642  2mo2  2681  2eu4  2688  sbabel  2963  neanior  3057  r19.26m  3130  reeanlem  3242  rexeqbii  3344  reu5  3378  cbvreuw  3402  cgsex4g  3509  reu2  3697  reu3  3699  2reu5a  3716  2reu5lem3  3729  2reu1  3859  eqss  3960  unss  4151  ralunb  4158  ssin  4199  undi  4246  indifdi  4255  undif3  4261  inab  4270  difab  4271  reuss2  4287  reupick  4290  2reu4lem  4489  reuprg  4674  sstp  4805  tpss  4806  prneimg  4823  prneimg2  4824  prnebg  4825  uniinOLD  4901  intun  4949  disjiun  5101  disjxiun  5110  brin  5167  brdif  5168  ssext  5436  pweqb  5438  opthg2  5462  copsex4g  5479  propeqop  5491  eqopab2bw  5534  eqopab2b  5538  pwin  5553  pofun  5588  dffr6  5618  wetrep  5655  elxp3  5728  soinxp  5744  weinxp  5747  csbxp  5763  relun  5799  inopab  5817  difopab  5818  inxp  5819  opelco2g  5854  cnvco  5876  dmin  5902  restidsing  6056  intasym  6116  asymref  6117  asymref2  6118  cnvdif  6141  xpnz  6157  difxp  6162  xpdifid  6166  xpdifcnvepel  6167  xp11  6174  dfco2  6247  cnvpo  6289  cnvso  6290  xpco  6291  reu3op  6294  dfpo2  6298  dffun4  6550  funun  6583  fun11  6611  fununi  6612  imadif  6621  fnres  6663  mptfnf  6671  fnopabg  6673  fun  6741  fin  6759  dff1o2  6827  brprcneu  6872  brprcneuALT  6873  dffv2  6977  fsn  7132  f13dfv  7273  dff1o6  7274  isotr  7335  eqoprab2bw  7481  eqoprab2b  7482  fvmpopr2d  7573  porpss  7725  epweon  7774  onsucb  7813  resf1extb  7931  elxp6  8020  dfoprab3  8051  opiota  8056  poxp  8124  soxp  8125  poxp2  8139  xpord2pred  8141  xpord2indlem  8143  xpord3pred  8148  xpord3inddlem  8150  soseq  8155  suppvalbr  8160  brtpos2  8228  frrlem9  8291  fprlem1  8297  tfrlem7  8370  dfer2  8695  eqer  8731  iiner  8787  uniinqs  8795  brecop  8808  eroveu  8810  erovlem  8811  fsetexb  8861  mapval2  8870  ixpin  8921  boxriin  8938  brsdom  8971  xpcomco  9055  xpassen  9059  sbthlem9  9083  sbthlem10  9084  brsdom2  9089  ssenen  9139  sbthfilem  9182  dffi3  9391  dfsup2  9404  infcllem  9448  axinf2  9609  zfinf2  9611  oemapso  9651  ttrcltr  9685  frrlem15  9729  scottexs  9861  scott0s  9862  kardex  9880  karden  9881  dfac5lem1  10107  dfac5lem3  10109  kmlem15  10148  enfin2i  10305  fin23lem34  10330  brdom7disj  10515  fpwwe2lem11  10626  fpwwe2lem12  10627  axgroth5  10809  grothprim  10819  addsrpr  11060  mulsrpr  11061  mulgt0sr  11090  addcnsr  11120  mulcnsr  11121  ltresr  11125  axcnre  11149  ssxr  11279  infrenegsup  12198  nnwos  12939  zmin  12968  xrnemnf  13142  xrnepnf  13143  xmullem  13290  xmulcom  13292  xmulneg1  13295  xmulf  13298  xrinfmss2  13337  elfzuzb  13546  fzass4  13590  seqof  14095  hashbclem  14489  hashfacen  14491  xpcogend  15011  trclublem  15032  rexanre  15398  caubnd  15410  o1lo1  15588  rpnnen2lem12  16281  lcmcllem  16654  lcmftp  16694  lcmfunsnlem2  16698  isprm3  16741  prmreclem2  16977  4sqlem12  17016  catcone0  17743  isffth2  17975  fucinv  18033  lublecllem  18414  odulub  18461  oduglb  18463  issubmgm  18760  rabsubmgmd  18762  mndpsuppss  18823  issubm  18861  issubmd  18864  0subm  18876  insubm  18877  sursubmefmnd  18955  injsubmefmnd  18956  smndex1mgm  18969  isnsg2  19222  cycsubm  19273  oppgid  19426  symgfixf1  19507  pmtrrn2  19530  lsmdisjr  19754  lsmhash  19775  gsumcom3  20048  dprd0  20103  issrg  20270  dvdsrtr  20450  isirred2  20503  isdomn3  20799  opprdomnb  20801  isdomn4r  20803  lss1d  21062  lspsolvlem  21244  lbsextlem2  21261  ssdifidllem  21453  cnfldfun  21505  unocv  21799  iunocv  21800  evlsval  22206  mpomatmul  22572  cpmidpmat  22999  tgval2  23082  fctop  23130  ppttop  23133  epttop  23135  cnnei  23408  2ndcctbss  23581  txuni2  23691  txbas  23693  ptbasin  23703  txdis1cn  23761  xkococnlem  23785  opnfbas  23968  fgcl  24004  fbasrn  24010  filuni  24011  cfinfil  24019  csdfil  24020  fin1aufil  24058  rnelfmlem  24078  fmfnfmlem3  24082  txflf  24132  xmeterval  24558  reconn  24955  iimulcl  25065  isclmp  25225  iscau3  25406  rrxmvallem  25532  minveclem3  25557  pmltpc  25578  ovolfcl  25594  ismbl  25654  dyaddisj  25724  iblre  25922  plyun0  26323  logfaclbnd  27352  lgslem3  27429  lgsdir2lem5  27459  nosupinfsep  27862  ltsrec  27960  madebdaylemlrcut  28058  addsproplem2  28129  addsuniflem  28160  negsproplem2  28188  negsid  28200  mulsproplem5  28279  mulsproplem6  28280  mulsproplem7  28281  mulsproplem8  28282  mulsproplem9  28283  mulsuniflem  28308  precsexlem9  28374  precsexlem10  28375  ons2ind  28434  nnaddscl  28505  nnmulscl  28506  zaddscl  28553  zsoring  28568  recut  28653  readdscl  28658  remulscl  28661  tgjustf  28708  ishpg  29000  usgrexmpllem  29551  nb3grpr2  29674  vtxd0nedgb  29779  wlk1walk  29929  clwlkcompbp  30072  wwlknllvtx  30136  wwlksonvtx  30145  wspthnonp  30149  wwlksn0s  30151  wwlksnndef  30195  2wlkdlem8  30223  elwwlks2s3  30241  clwwlkf1  30341  clwwlknonccat  30388  clwwlknon2x  30395  3pthdlem1  30456  upgr4cycl4dv4e  30477  frgr2wwlk1  30621  frgrreg  30686  ajfval  31102  issh  31501  chcon2i  31757  chcon3i  31759  spanuni  31837  5oalem7  31953  3oalem3  31957  pjin2i  32486  pjin3i  32487  cvnbtwn4  32582  mdslj1i  32612  mdslj2i  32613  mdslmd1i  32622  chrelat4i  32666  chirredi  32687  cdj3i  32734  rmoun  32781  difrab2  32785  eqdif  32806  inpr0  32819  iuninc  32846  fcoinvbr  32891  suppss2f  32924  fmptdF  32942  disjdsct  32989  f1od2  33005  hashxpe  33093  tosglblem  33235  mgcval  33248  pmtrprfv2  33349  elrgspnlem2  33504  ssmxidllem  33701  ccfldextdgrr  34007  fldext2chn  34063  ordtconnlem1  34259  esumpfinvalf  34411  esum2dlem  34427  measiuns  34552  eulerpartlemt0  34704  eulerpartlemr  34709  eulerpartlemn  34716  ballotlem2  34824  ballotlemodife  34833  bnj887  35099  bnj976  35111  bnj1385  35165  bnj153  35213  bnj543  35226  bnj607  35249  bnj882  35259  bnj916  35266  bnj983  35284  axreg  35473  axregscl  35474  axregs  35485  onvfowev  35533  derangenlem  35596  pconnconn  35656  fmlaomn0  35815  fmla0disjsuc  35823  fmlasucdisj  35824  elmpst  35961  xpab  36151  dftr6  36176  dffr5  36179  fundmpss  36192  elpotr  36204  brtxp  36303  brpprod  36308  brsset  36312  idsset  36313  dfon3  36315  ellimits  36333  dffun10  36337  elfuns  36338  brcart  36355  brimg  36360  brapply  36361  brcap  36363  lemsuccf  36364  funpartfun  36368  dfrecs2  36375  dfrdg4  36376  altopthc  36396  altopthd  36397  altopelaltxp  36401  outsideoftr  36554  rmoeqbii  36623  reueqbii  36625  rabeqbii  36629  riotaeqbii  36633  ixpeq1i  36635  cbvixpvw2  36680  cbvprodvw2  36682  trer  36750  neibastop1  36793  neifg  36805  df3nandALT1  36833  imnand2  36836  axtco  36905  regsfromregtco  36972  regsfromunir1  36974  mh-prprimbi  36977  eliminable-abelab  37428  bj-eldiag2  37743  bj-imdiridlem  37751  bj-opabco  37754  bj-xpcossxp  37755  topdifinfeq  37918  relowlssretop  37931  relowlpssretop  37932  wl-cases2-dnf  38089  poimirlem30  38223  poimirlem32  38225  ismblfin  38234  mbfposadd  38240  inixp  38301  elghomOLD  38460  keridl  38605  smprngopr  38625  sbcani  38681  inxpxrn  38991  dfcoss2  39076  cosscnv  39079  coss1cnvres  39080  coss2cnvepres  39081  1cossres  39092  dfcoels  39093  trressn  39108  br1cossinres  39110  br1cossinidres  39112  br1cossincnvepres  39113  br1cossxrnidres  39114  br1cossxrncnvepres  39115  cosscnvssid3  39139  coss0  39142  cossid  39143  trcoss  39145  eleccossin  39146  dfssr2  39152  br1cossxrncnvssrres  39161  refsymrels3  39223  refsymrel2  39224  refsymrel3  39225  elrefsymrels3  39227  dfeqvrel2  39247  dfeqvrel3  39248  redundeq1  39286  redundpbi1  39288  dfcomember3  39332  eqvreldmqs  39333  eqvreldmqs2  39334  dfeldisj3  39384  eldisjdmqsim  39390  eldisjn0elb  39418  antisymrelres  39439  dfmembpart2  39446  prtlem10  39563  prter1  39577  lcvbr3  39721  isopos  39878  llnexatN  40219  snatpsubN  40448  pclclN  40589  pclfinN  40598  lhpocnel2  40717  cdlemk19w  41670  dih1dimatlem  42027  psspwb  42923  redvmptabs  43045  mzpclall  43384  mzpincl  43391  mzpindd  43403  2nn0ind  43598  dford4  43682  wopprc  43683  islmodfg  43722  ifpan123g  44111  ifpan23  44112  ifpnot23  44130  ifpdfxor  44139  ifpidg  44143  ifpid1g  44146  ifpim23g  44147  ifpim123g  44152  ifpim1g  44153  ifp1bi  44154  ifpimimb  44156  ifpororb  44157  ifpor123g  44160  ifpbibib  44162  rp-isfinite6  44170  alephiso2  44210  undmrnresiss  44256  cotrintab  44266  brtrclfv2  44379  dfxor4  44418  snhesn  44438  dffrege76  44591  uneqsn  44677  expandan  44924  ismnuprim  44930  nzin  44954  onfrALTlem5  45177  onfrALTlem4  45178  undif3VD  45516  onfrALTlem5VD  45519  onfrALTlem4VD  45520  dfac5prim  45625  wfaxpr  45633  brpermmodel  45638  permac8prim  45649  ndisj2  45697  rexabsle  46059  ellimcabssub0  46259  limsupre2mpt  46370  limsupre3  46373  limsupre3mpt  46374  limsupre3uz  46376  limsupreuz  46377  liminfreuz  46443  fourierdlem103  46849  fourierdlem104  46850  fourierdlem112  46858  smflim  47417  smflim2  47446  smflimsuplem1  47460  smflimsup  47468  cfsetsnfsetf1  47719  2reu8i  47773  ichan  48127  clnbgrsym  48526  dfnbgr6  48545  upgrimpthslem2  48596  isgrlim  48670  usgrexmpl2trifr  48725  pgnbgreunbgrlem5  48811  pgnbgreunbgr  48813  2zlidl  48928  smprngprmrng  49027  islininds2  49183  zlmodzxzldeplem3  49201  2itscp  49480  reutruALT  49502  iinxp  49528  0funclem  49783  fucofulem2  50008  fuco2el  50009  catcinv  50096  2arwcatlem1  50292  dfrals2  50487  alsbii  50497  ralsbii  50498  cbvals  50502  als-no-surprise  50503  rals-no-surprise  50504