Theorem pm5.32i 578

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 577	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
3	1, 2	mpbi 233	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 400

This theorem is referenced by:  pm5.32ri  579  anbi2i  625  anabs5  662  abai  825  annotanannot  833  pm5.33  834  cases  1038  equsexvwOLD  2012  equsexv  2266  equsexALT  2430  2sb5rf  2485  2eu8  2721  eq2tri  2860  rexbiia  3209  reubiia  3343  rmobiia  3348  rabbiia  3419  ceqsrexbv  3598  euxfrw  3660  euxfr  3662  2reu5  3697  dfpss3  4014  eldifpr  4557  eldiftp  4584  eldifsn  4680  elrint  4879  elriin  4966  rabxp  5564  copsex2gb  5643  eliunxp  5672  dfres3  5823  restidsing  5889  ressn  6104  dflim2  6215  fncnv  6397  dff1o5  6599  respreima  6813  dff4  6844  dffo3  6845  f1ompt  6852  fsn  6874  fconst3  6953  fconst4  6954  eufnfv  6969  dff13  6991  f1mpt  6997  isocnv3  7064  isores2  7065  isoini  7070  eloprabga  7240  mpomptx  7244  resoprab  7249  elrnmpores  7267  ov6g  7292  dfwe2  7476  dflim3  7542  dflim4  7543  dfopab2  7732  dfoprab3s  7733  dfoprab3  7734  fparlem1  7790  fparlem2  7791  fsplit  7795  brtpos2  7881  dftpos3  7893  tpostpos  7895  dfsmo2  7967  dfrecs3  7992  tz7.48-1  8062  ondif1  8109  ondif2  8110  elixp2  8448  xpcomco  8590  eqinf  8932  infempty  8955  r0weon  9423  isinfcard  9503  dfac5lem1  9534  fpwwe  10057  axgroth6  10239  axgroth3  10242  elni2  10288  indpi  10318  recmulnq  10375  genpass  10420  lemul1a  11483  sup3  11585  elnn0z  11982  elznn0  11984  elznn  11985  eluz2b1  12307  eluz2b3  12310  elfz2nn0  12993  elfzo3  13049  shftidt2  14432  clim0  14855  fprod2dlem  15326  divalglem4  15737  ndvdsadd  15751  gcdaddmlem  15862  algfx  15914  isprm3  16017  isprm5  16041  isprm7  16042  xpsfrnel  16827  isacs2  16916  isfull2  17173  isfth2  17177  tosso  17638  odudlatb  17798  issubmndb  17962  nsgacs  18306  isgim2  18397  isabl2  18907  iscyg3  18998  iscrng2  19309  isdrng2  19505  drngprop  19506  issdrg2  19570  islmim2  19831  islpir2  20017  isnzr2  20029  iunocv  20370  ishil2  20408  islinds2  20502  ssntr  21663  isclo2  21693  isperf2  21757  isperf3  21758  nrmsep3  21960  isconn2  22019  iskgen3  22154  ptpjpre1  22176  tx1cn  22214  tx2cn  22215  hausdiag  22250  qustgplem  22726  istdrg2  22783  isngp2  23203  isngp3  23204  isnvc2  23305  isclmp  23702  iscvs  23732  isncvsngp  23754  ovoliunlem1  24106  ismbl2  24131  i1f1lem  24293  i1fres  24309  itg1climres  24318  pilem1  25046  ellogrn  25151  ellogdm  25230  1cubr  25428  atandm  25462  atandm2  25463  atandm3  25464  atandm4  25465  atans2  25517  eldmgm  25607  isfusgrcl  27111  nbgrel  27130  iscusgrvtx  27211  iscusgredg  27213  clwlkclwwlkflem  27789  isph  28605  h2hcau  28762  h2hlm  28763  issh2  28992  isch2  29006  h1dei  29333  elbdop2  29654  dfadj2  29668  cnvadj  29675  hhcno  29687  hhcnf  29688  eleigvec2  29741  riesz2  29849  rnbra  29890  elat2  30123  ofpreima  30428  mpomptxf  30442  f1od2  30483  maprnin  30493  xrofsup  30518  xrdifh  30529  prmidl0  31034  cmpcref  31203  ofcfval  31467  ispisys2  31522  1stmbfm  31628  2ndmbfm  31629  eulerpartlems  31728  eulerpartlemgc  31730  eulerpartlemv  31732  eulerpartlemd  31734  eulerpartlemr  31742  eulerpartlemn  31749  ballotlemodife  31865  sgn3da  31909  oddprm2  32036  bnj945  32155  bnj1172  32383  bnj1296  32403  snmlval  32691  eldm3  33110  frr2  33258  madeval2  33403  brtxp2  33455  brpprod3a  33460  dffun10  33488  elfuns  33489  brimg  33511  dfrdg4  33525  ellines  33726  opnrebl  33781  bj-ax12ig  34082  bj-equsexval  34106  bj-substw  34169  bj-csbsnlem  34344  bj-mpomptALT  34534  bj-elid6  34585  bj-eldiag  34591  bj-imdiridlem  34600  bj-imdirco  34605  taupilem3  34733  topdifinffinlem  34764  relowlssretop  34780  wl-dfclab  34993  istotbnd3  35209  isbnd2  35221  isbnd3b  35223  exidcl  35314  isdrngo2  35396  isdrngo3  35397  iscrngo2  35435  isdmn2  35493  isfldidl2  35507  isdmn3  35512  brres2  35689  eldmqsres  35703  brxrn2  35787  islshpat  36313  iscvlat2N  36620  ishlat3N  36650  snatpsubN  37046  diclspsn  38490  prjspeclsp  39606  isnacs2  39647  islnm2  40022  islnr2  40058  islnr3  40059  isdomn3  40148  iscard5  40242  en2pr  40246  pren2  40252  elinintab  40275  elmapintab  40296  elinlem  40298  cnvcnvintabd  40300  sqrtcvallem1  40331  reabsifneg  40332  reabsifpos  40334  k0004lem1  40850  dffo3f  41806  2reu8  43668  dfdfat2  43684  prproropf1olem0  44019  prprelb  44033  prprspr2  44035  isodd2  44153  iseven5  44182  isodd7  44183  oddprmne2  44233  ismhm0  44425  sgrp2sgrp  44488  0ringdif  44494  isrnghmmul  44517  eliunxp2  44735  mpomptx2  44736  elbigo  44965