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  27349  isfusgrcl  28609  nbgrel  28628  iscusgrvtx  28709  iscusgredg  28711  clwlkclwwlkflem  29288  isph  30106  h2hcau  30263  h2hlm  30264  issh2  30493  isch2  30507  h1dei  30834  elbdop2  31155  dfadj2  31169  cnvadj  31176  hhcno  31188  hhcnf  31189  eleigvec2  31242  riesz2  31350  rnbra  31391  elat2  31624  ofpreima  31921  mpomptxf  31936  f1od2  31977  maprnin  31987  xrofsup  32011  xrdifh  32022  prmidl0  32600  cmpcref  32861  ofcfval  33127  ispisys2  33182  1stmbfm  33290  2ndmbfm  33291  eulerpartlems  33390  eulerpartlemgc  33392  eulerpartlemv  33394  eulerpartlemd  33396  eulerpartlemr  33404  eulerpartlemn  33411  ballotlemodife  33527  sgn3da  33571  oddprm2  33698  bnj945  33815  bnj1172  34043  bnj1296  34063  snmlval  34353  eldm3  34762  brtxp2  34884  brpprod3a  34889  dffun10  34917  elfuns  34918  brimg  34940  dfrdg4  34954  ellines  35155  opnrebl  35253  bj-ax12ig  35561  bj-equsexval  35585  bj-substw  35648  bj-csbsnlem  35831  bj-clel3gALT  35977  bj-mpomptALT  36048  bj-elid6  36099  bj-eldiag  36105  bj-imdiridlem  36114  bj-imdirco  36119  bj-isrvec  36223  taupilem3  36248  topdifinffinlem  36276  relowlssretop  36292  wl-dfclab  36506  istotbnd3  36687  isbnd2  36699  isbnd3b  36701  exidcl  36792  isdrngo2  36874  isdrngo3  36875  iscrngo2  36913  isdmn2  36971  isfldidl2  36985  isdmn3  36990  brres2  37184  eldmqsres  37203  brxrn2  37293  petlem  37730  islshpat  37935  iscvlat2N  38242  ishlat3N  38272  snatpsubN  38669  diclspsn  40113  reelznn0nn  41370  prjspeclsp  41402  isnacs2  41492  islnm2  41868  islnr2  41904  islnr3  41905  isdomn3  41994  dflim7  42071  omge2  42096  minregex  42333  iscard5  42335  en2pr  42346  pren2  42352  elinintab  42374  elmapintab  42395  elinlem  42397  cnvcnvintabd  42399  sqrtcvallem1  42430  reabsifpos  42433  k0004lem1  42946  dffo3f  43925  2reu8  45868  dfdfat2  45884  prproropf1olem0  46218  prprelb  46232  prprspr2  46234  isodd2  46351  iseven5  46380  isodd7  46381  oddprmne2  46431  ismhm0  46623  sgrp2sgrp  46686  0ringdif  46692  isrnghmmul  46739  eliunxp2  47057  mpomptx2  47058  elbigo  47285  opndisj  47583  isnrm4  47611  iscnrm3  47633  iscnrm4  47635  catprs  47679