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  827  annotanannot  835  pm5.33  836  cases  1042  equsexALT  2423  2sb5rf  2476  2eu8  2658  eq2tri  2803  rexbiia  3091  rmobiia  3385  reubiia  3386  rabbiia  3438  rabbiiaOLD  3439  ceqsrexbv  3657  euxfrw  3731  euxfr  3733  2reu5  3768  dfpss3  4100  eldifpr  4664  eldiftp  4693  eldifsn  4792  elrint  4995  elriin  5087  rabxp  5738  copsex2gb  5820  eliunxp  5852  dfres3  6006  restidsing  6075  ressn  6310  dflim2  6446  fncnv  6644  dff1o5  6862  respreima  7090  dff4  7125  dffo3  7126  dffo3f  7130  f1ompt  7135  fsn  7159  fconst3  7237  fconst4  7238  eufnfv  7253  dff13  7279  f1mpt  7285  isocnv3  7356  isores2  7357  isoini  7362  eloprabga  7545  eloprabgaOLD  7546  mpomptx  7550  resoprab  7555  elrnmpores  7575  ov6g  7601  dfwe2  7797  dflim3  7872  dflim4  7873  dfopab2  8082  dfoprab3s  8083  dfoprab3  8084  fparlem1  8142  fparlem2  8143  fsplit  8147  brtpos2  8262  dftpos3  8274  tpostpos  8276  dfsmo2  8392  dfrecs3  8417  dfrecs3OLD  8418  tz7.48-1  8488  ondif1  8544  ondif2  8545  elixp2  8946  xpcomco  9107  pssnn  9213  enfi  9231  eqinf  9528  infempty  9551  ttrclselem2  9770  frr2  9804  r0weon  10056  isinfcard  10136  dfac5lem1  10167  fpwwe  10690  axgroth6  10872  axgroth3  10875  elni2  10921  indpi  10951  recmulnq  11008  genpass  11053  lemul1a  12125  sup3  12229  elnn0z  12630  elznn0  12632  elznn  12633  eluz2b1  12965  eluz2b3  12968  elfz2nn0  13661  elfzo3  13719  shftidt2  15123  clim0  15545  fprod2dlem  16019  divalglem4  16436  ndvdsadd  16450  gcdaddmlem  16564  algfx  16620  isprm3  16723  isprm5  16747  isprm7  16748  xpsfrnel  17615  isacs2  17704  isfull2  17971  isfth2  17975  tosso  18483  odudlatb  18589  ismhm0  18822  issubmndb  18837  nsgacs  19199  isgim2  19302  isabl2  19829  iscyg3  19925  iscrng2  20276  isrnghmmul  20465  isrim  20515  isnzr2  20541  0ringdif  20550  isdomn6  20737  isdomn3  20738  isdrng2  20766  drngprop  20767  issdrg2  20819  islmim2  21089  islpir2  21364  iunocv  21723  ishil2  21763  islinds2  21857  ssntr  23088  isclo2  23118  isperf2  23182  isperf3  23183  nrmsep3  23385  isconn2  23444  iskgen3  23579  ptpjpre1  23601  tx1cn  23639  tx2cn  23640  hausdiag  23675  qustgplem  24151  istdrg2  24208  isngp2  24632  isngp3  24633  isnvc2  24742  isclmp  25152  iscvs  25182  isncvsngp  25205  ovoliunlem1  25559  ismbl2  25584  i1f1lem  25746  i1fres  25763  itg1climres  25772  pilem1  26518  ellogrn  26624  ellogdm  26704  1cubr  26908  atandm  26942  atandm2  26943  atandm3  26944  atandm4  26945  atans2  26997  eldmgm  27088  madeval2  27915  elnns2  28367  elzs2  28408  elznns  28411  isfusgrcl  29361  nbgrel  29380  iscusgrvtx  29461  iscusgredg  29463  dfpth2  29772  clwlkclwwlkflem  30046  isph  30864  h2hcau  31021  h2hlm  31022  issh2  31251  isch2  31265  h1dei  31592  elbdop2  31913  dfadj2  31927  cnvadj  31934  hhcno  31946  hhcnf  31947  eleigvec2  32000  riesz2  32108  rnbra  32149  elat2  32382  ofpreima  32695  mpomptxf  32707  f1od2  32752  maprnin  32762  xrofsup  32791  xrdifh  32802  prmidl0  33471  cmpcref  33824  ofcfval  34092  ispisys2  34147  1stmbfm  34255  2ndmbfm  34256  eulerpartlems  34355  eulerpartlemgc  34357  eulerpartlemv  34359  eulerpartlemd  34361  eulerpartlemr  34369  eulerpartlemn  34376  ballotlemodife  34492  sgn3da  34536  oddprm2  34662  bnj945  34779  bnj1172  35007  bnj1296  35027  snmlval  35328  rexxfr3dALT  35636  eldm3  35753  brtxp2  35875  brpprod3a  35880  dffun10  35908  elfuns  35909  brimg  35931  dfrdg4  35945  ellines  36146  opnrebl  36315  bj-ax12ig  36631  bj-equsexval  36655  bj-substw  36717  bj-csbsnlem  36898  bj-clel3gALT  37043  bj-mpomptALT  37114  bj-elid6  37165  bj-eldiag  37171  bj-imdiridlem  37180  bj-imdirco  37185  bj-isrvec  37289  taupilem3  37314  topdifinffinlem  37342  relowlssretop  37358  wl-dfclab  37589  istotbnd3  37770  isbnd2  37782  isbnd3b  37784  exidcl  37875  isdrngo2  37957  isdrngo3  37958  iscrngo2  37996  isdmn2  38054  isfldidl2  38068  isdmn3  38073  brres2  38262  eldmqsres  38281  brxrn2  38369  petlem  38806  islshpat  39011  iscvlat2N  39318  ishlat3N  39348  snatpsubN  39745  diclspsn  41189  redvmptabs  42381  reelznn0nn  42470  prjspeclsp  42613  isnacs2  42708  islnm2  43081  islnr2  43117  islnr3  43118  dflim7  43277  omge2  43302  minregex  43538  iscard5  43540  en2pr  43551  pren2  43557  elinintab  43579  elmapintab  43600  elinlem  43602  cnvcnvintabd  43604  sqrtcvallem1  43635  reabsifpos  43638  k0004lem1  44151  2reu8  47073  dfdfat2  47089  prproropf1olem0  47438  prprelb  47452  prprspr2  47454  isodd2  47571  iseven5  47600  isodd7  47601  oddprmne2  47651  clnbgrel  47764  sclnbgrelself  47783  dfvopnbgr2  47788  sgrp2sgrp  48093  eliunxp2  48200  mpomptx2  48201  elbigo  48422  opndisj  48720  isnrm4  48748  iscnrm3  48770  iscnrm4  48772  catprs  48821