Theorem pm5.32i 576

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  pm5.32ri  577  anbi2i  624  anabs5  662  abai  826  annotanannot  834  pm5.33  835  cases  1042  equsexALT  2419  2sb5rf  2472  2eu8  2655  eq2tri  2800  rexbiia  3093  rmobiia  3383  reubiia  3384  rabbiia  3437  rabbiiaOLD  3438  ceqsrexbv  3645  euxfrw  3718  euxfr  3720  2reu5  3755  dfpss3  4087  eldifpr  4661  eldiftp  4691  eldifsn  4791  elrint  4996  elriin  5085  rabxp  5725  copsex2gb  5807  eliunxp  5838  dfres3  5987  restidsing  6053  ressn  6285  dflim2  6422  fncnv  6622  dff1o5  6843  respreima  7068  dff4  7103  dffo3  7104  f1ompt  7111  fsn  7133  fconst3  7215  fconst4  7216  eufnfv  7231  dff13  7254  f1mpt  7260  isocnv3  7329  isores2  7330  isoini  7335  eloprabga  7516  eloprabgaOLD  7517  mpomptx  7521  resoprab  7526  elrnmpores  7546  ov6g  7571  dfwe2  7761  dflim3  7836  dflim4  7837  dfopab2  8038  dfoprab3s  8039  dfoprab3  8040  fparlem1  8098  fparlem2  8099  fsplit  8103  brtpos2  8217  dftpos3  8229  tpostpos  8231  dfsmo2  8347  dfrecs3  8372  dfrecs3OLD  8373  tz7.48-1  8443  ondif1  8501  ondif2  8502  elixp2  8895  xpcomco  9062  pssnn  9168  enfi  9190  eqinf  9479  infempty  9502  ttrclselem2  9721  frr2  9755  r0weon  10007  isinfcard  10087  dfac5lem1  10118  fpwwe  10641  axgroth6  10823  axgroth3  10826  elni2  10872  indpi  10902  recmulnq  10959  genpass  11004  lemul1a  12068  sup3  12171  elnn0z  12571  elznn0  12573  elznn  12574  eluz2b1  12903  eluz2b3  12906  elfz2nn0  13592  elfzo3  13649  shftidt2  15028  clim0  15450  fprod2dlem  15924  divalglem4  16339  ndvdsadd  16353  gcdaddmlem  16465  algfx  16517  isprm3  16620  isprm5  16644  isprm7  16645  xpsfrnel  17508  isacs2  17597  isfull2  17862  isfth2  17866  tosso  18372  odudlatb  18478  issubmndb  18686  nsgacs  19042  isgim2  19139  isabl2  19658  iscyg3  19754  iscrng2  20075  isrim  20270  isnzr2  20297  isdrng2  20371  drngprop  20372  issdrg2  20411  islmim2  20677  islpir2  20889  iunocv  21234  ishil2  21274  islinds2  21368  ssntr  22562  isclo2  22592  isperf2  22656  isperf3  22657  nrmsep3  22859  isconn2  22918  iskgen3  23053  ptpjpre1  23075  tx1cn  23113  tx2cn  23114  hausdiag  23149  qustgplem  23625  istdrg2  23682  isngp2  24106  isngp3  24107  isnvc2  24216  isclmp  24613  iscvs  24643  isncvsngp  24666  ovoliunlem1  25019  ismbl2  25044  i1f1lem  25206  i1fres  25223  itg1climres  25232  pilem1  25963  ellogrn  26068  ellogdm  26147  1cubr  26347  atandm  26381  atandm2  26382  atandm3  26383  atandm4  26384  atans2  26436  eldmgm  26526  madeval2  27348  isfusgrcl  28578  nbgrel  28597  iscusgrvtx  28678  iscusgredg  28680  clwlkclwwlkflem  29257  isph  30075  h2hcau  30232  h2hlm  30233  issh2  30462  isch2  30476  h1dei  30803  elbdop2  31124  dfadj2  31138  cnvadj  31145  hhcno  31157  hhcnf  31158  eleigvec2  31211  riesz2  31319  rnbra  31360  elat2  31593  ofpreima  31890  mpomptxf  31905  f1od2  31946  maprnin  31956  xrofsup  31980  xrdifh  31991  prmidl0  32569  cmpcref  32830  ofcfval  33096  ispisys2  33151  1stmbfm  33259  2ndmbfm  33260  eulerpartlems  33359  eulerpartlemgc  33361  eulerpartlemv  33363  eulerpartlemd  33365  eulerpartlemr  33373  eulerpartlemn  33380  ballotlemodife  33496  sgn3da  33540  oddprm2  33667  bnj945  33784  bnj1172  34012  bnj1296  34032  snmlval  34322  eldm3  34731  brtxp2  34853  brpprod3a  34858  dffun10  34886  elfuns  34887  brimg  34909  dfrdg4  34923  ellines  35124  opnrebl  35205  bj-ax12ig  35513  bj-equsexval  35537  bj-substw  35600  bj-csbsnlem  35783  bj-clel3gALT  35929  bj-mpomptALT  36000  bj-elid6  36051  bj-eldiag  36057  bj-imdiridlem  36066  bj-imdirco  36071  bj-isrvec  36175  taupilem3  36200  topdifinffinlem  36228  relowlssretop  36244  wl-dfclab  36458  istotbnd3  36639  isbnd2  36651  isbnd3b  36653  exidcl  36744  isdrngo2  36826  isdrngo3  36827  iscrngo2  36865  isdmn2  36923  isfldidl2  36937  isdmn3  36942  brres2  37136  eldmqsres  37155  brxrn2  37245  petlem  37682  islshpat  37887  iscvlat2N  38194  ishlat3N  38224  snatpsubN  38621  diclspsn  40065  reelznn0nn  41322  prjspeclsp  41354  isnacs2  41444  islnm2  41820  islnr2  41856  islnr3  41857  isdomn3  41946  dflim7  42023  omge2  42048  minregex  42285  iscard5  42287  en2pr  42298  pren2  42304  elinintab  42326  elmapintab  42347  elinlem  42349  cnvcnvintabd  42351  sqrtcvallem1  42382  reabsifpos  42385  k0004lem1  42898  dffo3f  43877  2reu8  45820  dfdfat2  45836  prproropf1olem0  46170  prprelb  46184  prprspr2  46186  isodd2  46303  iseven5  46332  isodd7  46333  oddprmne2  46383  ismhm0  46575  sgrp2sgrp  46638  0ringdif  46644  isrnghmmul  46691  eliunxp2  47009  mpomptx2  47010  elbigo  47237  opndisj  47535  isnrm4  47563  iscnrm3  47585  iscnrm4  47587  catprs  47631