Theorem pm5.32i 574

Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)

Hypothesis

Ref	Expression
pm5.32i.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
pm5.32i	⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

Proof of Theorem pm5.32i

Step	Hyp	Ref	Expression
1		pm5.32i.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		pm5.32 573	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
3	1, 2	mpbi 230	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ 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:  pm5.32ri  575  anbi2i  623  anabs5  663  abai  826  annotanannot  834  pm5.33  835  cases  1042  equsexALT  2424  2sb5rf  2477  2eu8  2659  eq2tri  2798  rexbiia  3082  rmobiia  3370  reubiia  3371  rabbiia  3424  rabbiiaOLD  3425  ceqsrexbv  3640  euxfrw  3709  euxfr  3711  2reu5  3746  dfpss3  4069  eldifpr  4639  eldiftp  4668  eldifsn  4767  elrint  4970  elriin  5062  rabxp  5707  copsex2gb  5790  eliunxp  5822  dfres3  5976  restidsing  6045  ressn  6279  dflim2  6415  fncnv  6614  dff1o5  6832  respreima  7061  dff4  7096  dffo3  7097  dffo3f  7101  f1ompt  7106  fsn  7130  fconst3  7210  fconst4  7211  eufnfv  7226  dff13  7252  f1mpt  7259  isocnv3  7330  isores2  7331  isoini  7336  eloprabga  7521  mpomptx  7525  resoprab  7530  elrnmpores  7550  ov6g  7576  dfwe2  7773  dflim3  7847  dflim4  7848  dfopab2  8056  dfoprab3s  8057  dfoprab3  8058  fparlem1  8116  fparlem2  8117  fsplit  8121  brtpos2  8236  dftpos3  8248  tpostpos  8250  dfsmo2  8366  dfrecs3  8391  dfrecs3OLD  8392  tz7.48-1  8462  ondif1  8518  ondif2  8519  elixp2  8920  xpcomco  9081  pssnn  9187  enfi  9206  eqinf  9502  infempty  9526  ttrclselem2  9745  frr2  9779  r0weon  10031  isinfcard  10111  dfac5lem1  10142  fpwwe  10665  axgroth6  10847  axgroth3  10850  elni2  10896  indpi  10926  recmulnq  10983  genpass  11028  lemul1a  12100  sup3  12204  elnn0z  12606  elznn0  12608  elznn  12609  eluz2b1  12940  eluz2b3  12943  elfz2nn0  13640  elfzo3  13698  shftidt2  15105  clim0  15527  fprod2dlem  16001  divalglem4  16420  ndvdsadd  16434  gcdaddmlem  16548  algfx  16604  isprm3  16707  isprm5  16731  isprm7  16732  xpsfrnel  17581  isacs2  17670  isfull2  17931  isfth2  17935  tosso  18434  odudlatb  18540  ismhm0  18773  issubmndb  18788  nsgacs  19150  isgim2  19253  isabl2  19776  iscyg3  19872  iscrng2  20217  isrnghmmul  20407  isrim  20457  isnzr2  20483  0ringdif  20492  isdomn6  20679  isdomn3  20680  isdrng2  20708  drngprop  20709  issdrg2  20760  islmim2  21029  islpir2  21296  iunocv  21646  ishil2  21684  islinds2  21778  ssntr  23001  isclo2  23031  isperf2  23095  isperf3  23096  nrmsep3  23298  isconn2  23357  iskgen3  23492  ptpjpre1  23514  tx1cn  23552  tx2cn  23553  hausdiag  23588  qustgplem  24064  istdrg2  24121  isngp2  24541  isngp3  24542  isnvc2  24643  isclmp  25053  iscvs  25083  isncvsngp  25106  ovoliunlem1  25460  ismbl2  25485  i1f1lem  25647  i1fres  25663  itg1climres  25672  pilem1  26418  ellogrn  26525  ellogdm  26605  1cubr  26809  atandm  26843  atandm2  26844  atandm3  26845  atandm4  26846  atans2  26898  eldmgm  26989  madeval2  27818  elnns2  28290  elzs2  28344  elznns  28347  isfusgrcl  29305  nbgrel  29324  iscusgrvtx  29405  iscusgredg  29407  dfpth2  29716  clwlkclwwlkflem  29990  isph  30808  h2hcau  30965  h2hlm  30966  issh2  31195  isch2  31209  h1dei  31536  elbdop2  31857  dfadj2  31871  cnvadj  31878  hhcno  31890  hhcnf  31891  eleigvec2  31944  riesz2  32052  rnbra  32093  elat2  32326  ofpreima  32648  mpomptxf  32660  f1od2  32703  maprnin  32713  xrofsup  32749  xrdifh  32762  sgn3da  32818  prmidl0  33470  cmpcref  33886  ofcfval  34134  ispisys2  34189  1stmbfm  34297  2ndmbfm  34298  eulerpartlems  34397  eulerpartlemgc  34399  eulerpartlemv  34401  eulerpartlemd  34403  eulerpartlemr  34411  eulerpartlemn  34418  ballotlemodife  34535  oddprm2  34692  bnj945  34809  bnj1172  35037  bnj1296  35057  snmlval  35358  rexxfr3dALT  35666  eldm3  35783  brtxp2  35904  brpprod3a  35909  dffun10  35937  elfuns  35938  brimg  35960  dfrdg4  35974  ellines  36175  opnrebl  36343  bj-ax12ig  36659  bj-equsexval  36683  bj-substw  36745  bj-csbsnlem  36926  bj-clel3gALT  37071  bj-mpomptALT  37142  bj-elid6  37193  bj-eldiag  37199  bj-imdiridlem  37208  bj-imdirco  37213  bj-isrvec  37317  taupilem3  37342  topdifinffinlem  37370  relowlssretop  37386  wl-dfclab  37619  istotbnd3  37800  isbnd2  37812  isbnd3b  37814  exidcl  37905  isdrngo2  37987  isdrngo3  37988  iscrngo2  38026  isdmn2  38084  isfldidl2  38098  isdmn3  38103  brres2  38291  eldmqsres  38310  brxrn2  38398  petlem  38835  islshpat  39040  iscvlat2N  39347  ishlat3N  39377  snatpsubN  39774  diclspsn  41218  redvmptabs  42378  reelznn0nn  42467  prjspeclsp  42610  isnacs2  42704  islnm2  43077  islnr2  43113  islnr3  43114  dflim7  43272  omge2  43297  minregex  43533  iscard5  43535  en2pr  43546  pren2  43552  elinintab  43574  elmapintab  43595  elinlem  43597  cnvcnvintabd  43599  sqrtcvallem1  43630  reabsifpos  43633  k0004lem1  44146  2reu8  47121  dfdfat2  47137  prproropf1olem0  47496  prprelb  47510  prprspr2  47512  isodd2  47629  iseven5  47658  isodd7  47659  oddprmne2  47709  clnbgrel  47822  sclnbgrelself  47841  dfvopnbgr2  47846  sgrp2sgrp  48183  eliunxp2  48289  mpomptx2  48290  elbigo  48511  tposres0  48832  opndisj  48857  isnrm4  48885  iscnrm3  48906  iscnrm4  48908  catprs  48966  initopropd  49140  termopropd  49141  zeroopropd  49142  2arwcatlem1  49452  setc1onsubc  49459