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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anbi12ci  629  an2anr  636  ordi  1007  ordir  1008  orddi  1011  pm5.17  1013  xor  1016  cases2  1047  3anbi123i  1155  an6  1447  nanbi  1500  cadan  1609  nic-axALT  1674  19.43OLD  1883  sbbi  2307  aaan  2331  sbnf2  2356  eubii  2578  cbveuvw  2598  cbveuw  2599  cbveuALT  2601  2mo2  2640  2eu4  2648  sbabel  2924  neanior  3018  r19.26m  3088  reeanlem  3200  rexeqbii  3308  reu5  3345  cbvreuw  3371  cgsex4g  3483  reu2  3685  reu3  3687  2reu5a  3704  2reu5lem3  3717  2reu1  3849  eqss  3951  unss  4141  ralunb  4148  ssin  4190  undi  4236  indifdi  4245  undif3  4251  inab  4260  difab  4261  reuss2  4277  reupick  4280  2reu4lem  4473  reuprg  4655  sstp  4787  tpss  4788  prneimg  4805  prneimg2  4806  prnebg  4807  uniin  4882  intun  4930  disjiun  5080  disjxiun  5089  brin  5144  brdif  5145  ssext  5397  pweqb  5399  opthg2  5422  copsex4g  5438  propeqop  5450  eqopab2bw  5491  eqopab2b  5495  pwin  5510  pofun  5545  dffr6  5575  wetrep  5612  elxp3  5685  soinxp  5701  weinxp  5704  csbxp  5719  relun  5754  inopab  5772  difopab  5773  inxp  5774  inxpOLD  5775  opelco2g  5810  cnvco  5828  dmin  5854  restidsing  6004  intasym  6064  asymref  6065  asymref2  6066  cnvdif  6092  xpnz  6108  difxp  6113  xpdifid  6117  xp11  6124  dfco2  6194  cnvpo  6235  cnvso  6236  xpco  6237  reu3op  6240  dfpo2  6244  dffun4  6495  funun  6528  fun11  6556  fununi  6557  imadif  6566  fnres  6609  mptfnf  6617  fnopabg  6619  fun  6686  fin  6704  dff1o2  6769  brprcneu  6812  brprcneuALT  6813  dffv2  6918  fsn  7069  f13dfv  7211  dff1o6  7212  isotr  7273  eqoprab2bw  7419  eqoprab2b  7420  fvmpopr2d  7511  porpss  7663  epweon  7711  onsucb  7750  resf1extb  7867  elxp6  7958  dfoprab3  7989  opiota  7994  poxp  8061  soxp  8062  poxp2  8076  xpord2pred  8078  xpord2indlem  8080  xpord3pred  8085  xpord3inddlem  8087  soseq  8092  suppvalbr  8097  brtpos2  8165  frrlem9  8227  fprlem1  8233  tfrlem7  8305  dfer2  8626  eqer  8661  iiner  8716  uniinqs  8724  brecop  8737  eroveu  8739  erovlem  8740  fsetexb  8791  mapval2  8799  ixpin  8850  boxriin  8867  brsdom  8900  xpcomco  8984  xpassen  8988  sbthlem9  9012  sbthlem10  9013  brsdom2  9018  ssenen  9068  sbthfilem  9112  dffi3  9321  dfsup2  9334  infcllem  9378  axinf2  9536  zfinf2  9538  oemapso  9578  ttrcltr  9612  frrlem15  9653  scottexs  9783  scott0s  9784  kardex  9790  karden  9791  dfac5lem1  10017  dfac5lem3  10019  kmlem15  10059  enfin2i  10215  fin23lem34  10240  brdom7disj  10425  fpwwe2lem11  10535  fpwwe2lem12  10536  axgroth5  10718  grothprim  10728  addsrpr  10969  mulsrpr  10970  mulgt0sr  10999  addcnsr  11029  mulcnsr  11030  ltresr  11034  axcnre  11058  ssxr  11185  infrenegsup  12108  nnwos  12816  zmin  12845  xrnemnf  13019  xrnepnf  13020  xmullem  13166  xmulcom  13168  xmulneg1  13171  xmulf  13174  xrinfmss2  13213  elfzuzb  13421  fzass4  13465  seqof  13966  hashbclem  14359  hashfacen  14361  xpcogend  14881  trclublem  14902  rexanre  15254  caubnd  15266  o1lo1  15444  rpnnen2lem12  16134  lcmcllem  16507  lcmftp  16547  lcmfunsnlem2  16551  isprm3  16594  prmreclem2  16829  4sqlem12  16868  catcone0  17593  isffth2  17825  fucinv  17883  lublecllem  18264  odulub  18311  oduglb  18313  issubmgm  18576  rabsubmgmd  18578  mndpsuppss  18639  issubm  18677  issubmd  18680  0subm  18691  insubm  18692  sursubmefmnd  18770  injsubmefmnd  18771  smndex1mgm  18781  isnsg2  19035  cycsubm  19081  oppgid  19235  symgfixf1  19316  pmtrrn2  19339  lsmdisjr  19563  lsmhash  19584  gsumcom3  19857  dprd0  19912  issrg  20073  dvdsrtr  20253  isirred2  20306  isdomn3  20600  opprdomnb  20602  isdomn4r  20604  lss1d  20866  lspsolvlem  21049  lbsextlem2  21066  cnfldfun  21275  cnfldfunOLD  21288  unocv  21587  iunocv  21588  evlsval  21991  mpomatmul  22331  cpmidpmat  22758  tgval2  22841  fctop  22889  ppttop  22892  epttop  22894  cnnei  23167  2ndcctbss  23340  txuni2  23450  txbas  23452  ptbasin  23462  txdis1cn  23520  xkococnlem  23544  opnfbas  23727  fgcl  23763  fbasrn  23769  filuni  23770  cfinfil  23778  csdfil  23779  fin1aufil  23817  rnelfmlem  23837  fmfnfmlem3  23841  txflf  23891  xmeterval  24318  reconn  24715  iimulcl  24831  isclmp  24995  iscau3  25176  rrxmvallem  25302  minveclem3  25327  pmltpc  25349  ovolfcl  25365  ismbl  25425  dyaddisj  25495  iblre  25693  plyun0  26100  logfaclbnd  27131  lgslem3  27208  lgsdir2lem5  27238  nosupinfsep  27642  sltrec  27732  madebdaylemlrcut  27813  addsproplem2  27882  addsuniflem  27913  negsproplem2  27940  negsid  27952  mulsproplem5  28028  mulsproplem6  28029  mulsproplem7  28030  mulsproplem8  28031  mulsproplem9  28032  mulsuniflem  28057  precsexlem9  28122  precsexlem10  28123  nnaddscl  28243  nnmulscl  28244  zaddscl  28287  zsoring  28301  recut  28365  0reno  28366  readdscl  28368  remulscl  28371  tgjustf  28418  ishpg  28704  usgrexmpllem  29205  nb3grpr2  29328  vtxd0nedgb  29434  wlk1walk  29584  clwlkcompbp  29727  wwlknllvtx  29791  wwlksonvtx  29800  wspthnonp  29804  wwlksn0s  29806  wwlksnndef  29850  2wlkdlem8  29878  elwwlks2s3  29896  clwwlkf1  29993  clwwlknonccat  30040  clwwlknon2x  30047  3pthdlem1  30108  upgr4cycl4dv4e  30129  frgr2wwlk1  30273  frgrreg  30338  ajfval  30753  issh  31152  chcon2i  31408  chcon3i  31410  spanuni  31488  5oalem7  31604  3oalem3  31608  pjin2i  32137  pjin3i  32138  cvnbtwn4  32233  mdslj1i  32263  mdslj2i  32264  mdslmd1i  32273  chrelat4i  32317  chirredi  32338  cdj3i  32385  rmoun  32438  difrab2  32442  eqdif  32463  inpr0  32476  iuninc  32504  fcoinvbr  32549  suppss2f  32581  fmptdF  32599  disjdsct  32645  f1od2  32663  hashxpe  32752  tosglblem  32916  mgcval  32929  pmtrprfv2  33030  elrgspnlem2  33183  ssdifidllem  33393  ssmxidllem  33410  ccfldextdgrr  33639  fldext2chn  33695  ordtconnlem1  33891  esumpfinvalf  34043  esum2dlem  34059  measiuns  34184  eulerpartlemt0  34337  eulerpartlemr  34342  eulerpartlemn  34349  ballotlem2  34457  ballotlemodife  34466  bnj887  34732  bnj976  34744  bnj1385  34799  bnj153  34847  bnj543  34860  bnj607  34883  bnj882  34893  bnj916  34900  bnj983  34918  axreg  35062  axregscl  35063  axregs  35078  derangenlem  35148  pconnconn  35208  fmlaomn0  35367  fmla0disjsuc  35375  fmlasucdisj  35376  elmpst  35513  xpab  35703  dftr6  35728  dffr5  35731  fundmpss  35744  elpotr  35759  brtxp  35858  brpprod  35863  brsset  35867  idsset  35868  dfon3  35870  ellimits  35888  dffun10  35892  elfuns  35893  brcart  35910  brimg  35915  brapply  35916  brcap  35918  brsuccf  35919  funpartfun  35921  dfrecs2  35928  dfrdg4  35929  altopthc  35949  altopthd  35950  altopelaltxp  35954  outsideoftr  36107  rmoeqbii  36166  reueqbii  36168  rabeqbii  36172  riotaeqbii  36176  ixpeq1i  36178  cbvixpvw2  36223  cbvprodvw2  36225  trer  36294  neibastop1  36337  neifg  36349  df3nandALT1  36377  imnand2  36380  eliminable-abelab  36848  bj-eldiag2  37155  bj-imdiridlem  37163  bj-opabco  37166  bj-xpcossxp  37167  topdifinfeq  37328  relowlssretop  37341  relowlpssretop  37342  wl-cases2-dnf  37490  poimirlem30  37634  poimirlem32  37636  ismblfin  37645  mbfposadd  37651  inixp  37712  elghomOLD  37871  keridl  38016  smprngopr  38036  sbcani  38092  inxpxrn  38371  dfcoss2  38394  cosscnv  38397  coss1cnvres  38398  coss2cnvepres  38399  1cossres  38410  dfcoels  38411  trressn  38426  br1cossinres  38428  br1cossinidres  38430  br1cossincnvepres  38431  br1cossxrnidres  38432  br1cossxrncnvepres  38433  cosscnvssid3  38457  coss0  38460  cossid  38461  trcoss  38463  eleccossin  38464  dfssr2  38480  br1cossxrncnvssrres  38489  refsymrels3  38547  refsymrel2  38548  refsymrel3  38549  elrefsymrels3  38551  dfeqvrel2  38571  dfeqvrel3  38572  redundeq1  38610  redundpbi1  38612  dfcomember3  38656  eqvreldmqs  38657  eqvreldmqs2  38658  dfeldisj3  38701  eldisjn0elb  38727  antisymrelres  38745  dfmembpart2  38752  prtlem10  38848  prter1  38862  lcvbr3  39006  isopos  39163  llnexatN  39504  snatpsubN  39733  pclclN  39874  pclfinN  39883  lhpocnel2  40002  cdlemk19w  40955  dih1dimatlem  41312  psspwb  42205  redvmptabs  42337  mzpclall  42704  mzpincl  42711  mzpindd  42723  2nn0ind  42922  dford4  43006  wopprc  43007  islmodfg  43046  ifpan123g  43436  ifpan23  43437  ifpnot23  43455  ifpdfxor  43464  ifpidg  43468  ifpid1g  43471  ifpim23g  43472  ifpim123g  43477  ifpim1g  43478  ifp1bi  43479  ifpimimb  43481  ifpororb  43482  ifpor123g  43485  ifpbibib  43487  rp-isfinite6  43495  alephiso2  43535  undmrnresiss  43581  cotrintab  43591  brtrclfv2  43704  dfxor4  43743  snhesn  43763  dffrege76  43916  uneqsn  44002  expandan  44265  ismnuprim  44271  nzin  44295  onfrALTlem5  44520  onfrALTlem4  44521  undif3VD  44859  onfrALTlem5VD  44862  onfrALTlem4VD  44863  dfac5prim  44968  wfaxpr  44976  brpermmodel  44981  permac8prim  44992  ndisj2  45033  rexabsle  45402  ellimcabssub0  45602  limsupre2mpt  45715  limsupre3  45718  limsupre3mpt  45719  limsupre3uz  45721  limsupreuz  45722  liminfreuz  45788  fourierdlem103  46194  fourierdlem104  46195  fourierdlem112  46203  smflim  46762  smflim2  46791  smflimsuplem1  46805  smflimsup  46813  cfsetsnfsetf1  47047  2reu8i  47101  ichan  47443  clnbgrsym  47826  dfnbgr6  47845  upgrimpthslem2  47896  isgrlim  47970  usgrexmpl2trifr  48025  pgnbgreunbgrlem5  48111  pgnbgreunbgr  48113  2zlidl  48228  islininds2  48473  zlmodzxzldeplem3  48491  2itscp  48770  reutruALT  48793  iinxp  48819  0funclem  49075  fucofulem2  49300  fuco2el  49301  catcinv  49388  2arwcatlem1  49584  alsi-no-surprise  49785