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  2423  2sb5rf  2476  2eu8  2659  eq2tri  2798  rexbiia  3081  rmobiia  3356  reubiia  3357  rabbiia  3403  ceqsrexbv  3610  euxfrw  3679  euxfr  3681  2reu5  3716  dfpss3  4041  eldifpr  4615  eldiftp  4644  eldifsn  4742  elrint  4944  elriin  5036  rabxp  5672  copsex2gb  5755  eliunxp  5786  dfres3  5943  restidsing  6012  ressn  6243  dflim2  6375  fncnv  6565  dff1o5  6783  respreima  7011  dff4  7046  dffo3  7047  dffo3f  7051  f1ompt  7056  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  8054  fparlem2  8055  fsplit  8059  brtpos2  8174  dftpos3  8186  tpostpos  8188  dfsmo2  8279  dfrecs3  8304  tz7.48-1  8374  ondif1  8428  ondif2  8429  elixp2  8839  xpcomco  8995  pssnn  9093  enfi  9111  eqinf  9388  infempty  9412  ttrclselem2  9635  frr2  9672  r0weon  9922  isinfcard  10002  dfac5lem1  10033  fpwwe  10557  axgroth6  10739  axgroth3  10742  elni2  10788  indpi  10818  recmulnq  10875  genpass  10920  lemul1a  11995  sup3  12099  elnn0z  12501  elznn0  12503  elznn  12504  eluz2b1  12832  eluz2b3  12835  elfz2nn0  13534  elfzo3  13592  shftidt2  15004  clim0  15429  fprod2dlem  15903  divalglem4  16323  ndvdsadd  16337  gcdaddmlem  16451  algfx  16507  isprm3  16610  isprm5  16634  isprm7  16635  xpsfrnel  17483  isacs2  17576  isfull2  17837  isfth2  17841  tosso  18340  odudlatb  18448  ismhm0  18715  issubmndb  18730  nsgacs  19091  isgim2  19194  isabl2  19719  iscyg3  19815  iscrng2  20187  isrnghmmul  20378  isrim  20427  isnzr2  20451  0ringdif  20460  isdomn6  20647  isdomn3  20648  isdrng2  20676  drngprop  20677  issdrg2  20728  islmim2  21018  islpir2  21285  iunocv  21636  ishil2  21674  islinds2  21768  ssntr  23002  isclo2  23032  isperf2  23096  isperf3  23097  nrmsep3  23299  isconn2  23358  iskgen3  23493  ptpjpre1  23515  tx1cn  23553  tx2cn  23554  hausdiag  23589  qustgplem  24065  istdrg2  24122  isngp2  24541  isngp3  24542  isnvc2  24643  isclmp  25053  iscvs  25083  isncvsngp  25105  ovoliunlem1  25459  ismbl2  25484  i1f1lem  25646  i1fres  25662  itg1climres  25671  pilem1  26417  ellogrn  26524  ellogdm  26604  1cubr  26808  atandm  26842  atandm2  26843  atandm3  26844  atandm4  26845  atans2  26897  eldmgm  26988  madeval2  27829  elnns2  28337  elzs2  28395  elznns  28398  elreno2  28491  isfusgrcl  29394  nbgrel  29413  iscusgrvtx  29494  iscusgredg  29496  dfpth2  29802  clwlkclwwlkflem  30079  isph  30897  h2hcau  31054  h2hlm  31055  issh2  31284  isch2  31298  h1dei  31625  elbdop2  31946  dfadj2  31960  cnvadj  31967  hhcno  31979  hhcnf  31980  eleigvec2  32033  riesz2  32141  rnbra  32182  elat2  32415  ofpreima  32743  mpomptxf  32757  f1od2  32798  maprnin  32810  xrofsup  32847  xrdifh  32860  sgn3da  32915  prmidl0  33531  cmpcref  34007  ofcfval  34255  ispisys2  34310  1stmbfm  34417  2ndmbfm  34418  eulerpartlems  34517  eulerpartlemgc  34519  eulerpartlemv  34521  eulerpartlemd  34523  eulerpartlemr  34531  eulerpartlemn  34538  ballotlemodife  34655  oddprm2  34812  bnj945  34929  bnj1172  35157  bnj1296  35177  snmlval  35525  rexxfr3dALT  35833  eldm3  35955  brtxp2  36073  brpprod3a  36078  dffun10  36106  elfuns  36107  brimg  36129  dfrdg4  36145  ellines  36346  opnrebl  36514  bj-ax12ig  36836  bj-equsexval  36861  bj-substw  36923  bj-csbsnlem  37104  bj-clel3gALT  37249  bj-mpomptALT  37320  bj-elid6  37371  bj-eldiag  37377  bj-imdiridlem  37386  bj-imdirco  37391  bj-isrvec  37495  taupilem3  37520  topdifinffinlem  37548  relowlssretop  37564  wl-dfclab  37786  istotbnd3  37968  isbnd2  37980  isbnd3b  37982  exidcl  38073  isdrngo2  38155  isdrngo3  38156  iscrngo2  38194  isdmn2  38252  isfldidl2  38266  isdmn3  38271  brres2  38462  eldmqsres  38482  brxrn2  38565  blockadjliftmap  38629  petlem  39067  islshpat  39273  iscvlat2N  39580  ishlat3N  39610  snatpsubN  40006  diclspsn  41450  redvmptabs  42611  reelznn0nn  42712  prjspeclsp  42851  isnacs2  42944  islnm2  43316  islnr2  43352  islnr3  43353  dflim7  43511  omge2  43536  minregex  43771  iscard5  43773  en2pr  43784  pren2  43790  elinintab  43812  elmapintab  43833  elinlem  43835  cnvcnvintabd  43837  sqrtcvallem1  43868  reabsifpos  43871  k0004lem1  44384  2reu8  47354  dfdfat2  47370  prproropf1olem0  47744  prprelb  47758  prprspr2  47760  isodd2  47877  iseven5  47906  isodd7  47907  oddprmne2  47957  clnbgrel  48070  sclnbgrelself  48090  dfvopnbgr2  48095  sgrp2sgrp  48470  eliunxp2  48576  mpomptx2  48577  elbigo  48793  tposres0  49118  opndisj  49144  isnrm4  49172  iscnrm3  49193  iscnrm4  49195  catprs  49252  initopropd  49484  termopropd  49485  zeroopropd  49486  catcsect  49639  2arwcatlem1  49836  setc1onsubc  49843