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  624  anabs5  664  abai  827  annotanannot  835  pm5.33  836  cases  1043  equsexALT  2424  2sb5rf  2477  2eu8  2660  eq2tri  2799  rexbiia  3083  rmobiia  3349  reubiia  3350  rabbiia  3394  ceqsrexbv  3599  euxfrw  3668  euxfr  3670  2reu5  3705  dfpss3  4030  eldifpr  4603  eldiftp  4632  eldifsn  4730  elrint  4932  elriin  5024  rabxp  5670  copsex2gb  5753  eliunxp  5784  dfres3  5941  restidsing  6010  ressn  6241  dflim2  6373  fncnv  6563  dff1o5  6781  respreima  7010  dff4  7045  dffo3  7046  dffo3f  7050  f1ompt  7055  fsn  7080  fconst3  7159  fconst4  7160  eufnfv  7175  dff13  7200  f1mpt  7207  isocnv3  7278  isores2  7279  isoini  7284  eloprabga  7467  mpomptx  7471  resoprab  7476  elrnmpores  7496  ov6g  7522  dfwe2  7719  dflim3  7789  dflim4  7790  dfopab2  7996  dfoprab3s  7997  dfoprab3  7998  fparlem1  8053  fparlem2  8054  fsplit  8058  brtpos2  8173  dftpos3  8185  tpostpos  8187  dfsmo2  8278  dfrecs3  8303  tz7.48-1  8373  ondif1  8427  ondif2  8428  elixp2  8840  xpcomco  8996  pssnn  9094  enfi  9112  eqinf  9389  infempty  9413  ttrclselem2  9636  frr2  9673  r0weon  9923  isinfcard  10003  dfac5lem1  10034  fpwwe  10558  axgroth6  10740  axgroth3  10743  elni2  10789  indpi  10819  recmulnq  10876  genpass  10921  lemul1a  11996  sup3  12100  elnn0z  12502  elznn0  12504  elznn  12505  eluz2b1  12833  eluz2b3  12836  elfz2nn0  13535  elfzo3  13593  shftidt2  15005  clim0  15430  fprod2dlem  15904  divalglem4  16324  ndvdsadd  16338  gcdaddmlem  16452  algfx  16508  isprm3  16611  isprm5  16635  isprm7  16636  xpsfrnel  17484  isacs2  17577  isfull2  17838  isfth2  17842  tosso  18341  odudlatb  18449  ismhm0  18716  issubmndb  18731  nsgacs  19095  isgim2  19198  isabl2  19723  iscyg3  19819  iscrng2  20191  isrnghmmul  20380  isrim  20429  isnzr2  20453  0ringdif  20462  isdomn6  20649  isdomn3  20650  isdrng2  20678  drngprop  20679  issdrg2  20730  islmim2  21020  islpir2  21287  iunocv  21638  ishil2  21676  islinds2  21770  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  24540  isngp3  24541  isnvc2  24642  isclmp  25042  iscvs  25072  isncvsngp  25094  ovoliunlem1  25447  ismbl2  25472  i1f1lem  25634  i1fres  25650  itg1climres  25659  pilem1  26401  ellogrn  26508  ellogdm  26588  1cubr  26792  atandm  26826  atandm2  26827  atandm3  26828  atandm4  26829  atans2  26881  eldmgm  26972  madeval2  27813  elnns2  28321  elzs2  28379  elznns  28382  elreno2  28475  isfusgrcl  29378  nbgrel  29397  iscusgrvtx  29478  iscusgredg  29480  dfpth2  29786  clwlkclwwlkflem  30063  isph  30882  h2hcau  31039  h2hlm  31040  issh2  31269  isch2  31283  h1dei  31610  elbdop2  31931  dfadj2  31945  cnvadj  31952  hhcno  31964  hhcnf  31965  eleigvec2  32018  riesz2  32126  rnbra  32167  elat2  32400  ofpreima  32727  mpomptxf  32740  f1od2  32781  maprnin  32793  xrofsup  32830  xrdifh  32843  sgn3da  32898  prmidl0  33515  cmpcref  34000  ofcfval  34248  ispisys2  34303  1stmbfm  34410  2ndmbfm  34411  eulerpartlems  34510  eulerpartlemgc  34512  eulerpartlemv  34514  eulerpartlemd  34516  eulerpartlemr  34524  eulerpartlemn  34531  ballotlemodife  34648  oddprm2  34805  bnj945  34922  bnj1172  35149  bnj1296  35169  snmlval  35519  rexxfr3dALT  35827  eldm3  35949  brtxp2  36067  brpprod3a  36072  dffun10  36100  elfuns  36101  brimg  36123  dfrdg4  36139  ellines  36340  opnrebl  36508  bj-ax12ig  36913  bj-equsexval  36952  bj-substw  37020  bj-csbsnlem  37208  bj-clel3gALT  37353  bj-mpomptALT  37429  bj-elid6  37482  bj-eldiag  37488  bj-imdiridlem  37497  bj-imdirco  37502  bj-isrvec  37606  taupilem3  37631  topdifinffinlem  37659  relowlssretop  37675  wl-dfclab  37901  istotbnd3  38083  isbnd2  38095  isbnd3b  38097  exidcl  38188  isdrngo2  38270  isdrngo3  38271  iscrngo2  38309  isdmn2  38367  isfldidl2  38381  isdmn3  38386  brres2  38585  eldmqsres  38605  brxrn2  38696  blockadjliftmap  38770  qmapeldisjsim  39172  petlem  39227  eldisjs7  39253  petseq  39288  islshpat  39454  iscvlat2N  39761  ishlat3N  39791  snatpsubN  40187  diclspsn  41631  redvmptabs  42791  reelznn0nn  42905  prjspeclsp  43044  isnacs2  43137  islnm2  43509  islnr2  43545  islnr3  43546  dflim7  43704  omge2  43729  minregex  43964  iscard5  43966  en2pr  43977  pren2  43983  elinintab  44005  elmapintab  44026  elinlem  44028  cnvcnvintabd  44030  sqrtcvallem1  44061  reabsifpos  44064  k0004lem1  44577  2reu8  47546  dfdfat2  47562  prproropf1olem0  47936  prprelb  47950  prprspr2  47952  isodd2  48069  iseven5  48098  isodd7  48099  oddprmne2  48149  clnbgrel  48262  sclnbgrelself  48282  dfvopnbgr2  48287  sgrp2sgrp  48662  eliunxp2  48768  mpomptx2  48769  elbigo  48985  tposres0  49310  opndisj  49336  isnrm4  49364  iscnrm3  49385  iscnrm4  49387  catprs  49444  initopropd  49676  termopropd  49677  zeroopropd  49678  catcsect  49831  2arwcatlem1  50028  setc1onsubc  50035