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  622  anabs5  662  abai  826  annotanannot  834  pm5.33  835  cases  1043  equsexALT  2427  2sb5rf  2480  2eu8  2662  eq2tri  2807  rexbiia  3098  rmobiia  3394  reubiia  3395  rabbiia  3447  rabbiiaOLD  3448  ceqsrexbv  3669  euxfrw  3743  euxfr  3745  2reu5  3780  dfpss3  4112  eldifpr  4680  eldiftp  4710  eldifsn  4811  elrint  5013  elriin  5104  rabxp  5748  copsex2gb  5830  eliunxp  5862  dfres3  6014  restidsing  6082  ressn  6316  dflim2  6452  fncnv  6651  dff1o5  6871  respreima  7099  dff4  7135  dffo3  7136  dffo3f  7140  f1ompt  7145  fsn  7169  fconst3  7250  fconst4  7251  eufnfv  7266  dff13  7292  f1mpt  7298  isocnv3  7368  isores2  7369  isoini  7374  eloprabga  7558  eloprabgaOLD  7559  mpomptx  7563  resoprab  7568  elrnmpores  7588  ov6g  7614  dfwe2  7809  dflim3  7884  dflim4  7885  dfopab2  8093  dfoprab3s  8094  dfoprab3  8095  fparlem1  8153  fparlem2  8154  fsplit  8158  brtpos2  8273  dftpos3  8285  tpostpos  8287  dfsmo2  8403  dfrecs3  8428  dfrecs3OLD  8429  tz7.48-1  8499  ondif1  8557  ondif2  8558  elixp2  8959  xpcomco  9128  pssnn  9234  enfi  9253  eqinf  9553  infempty  9576  ttrclselem2  9795  frr2  9829  r0weon  10081  isinfcard  10161  dfac5lem1  10192  fpwwe  10715  axgroth6  10897  axgroth3  10900  elni2  10946  indpi  10976  recmulnq  11033  genpass  11078  lemul1a  12148  sup3  12252  elnn0z  12652  elznn0  12654  elznn  12655  eluz2b1  12984  eluz2b3  12987  elfz2nn0  13675  elfzo3  13733  shftidt2  15130  clim0  15552  fprod2dlem  16028  divalglem4  16444  ndvdsadd  16458  gcdaddmlem  16570  algfx  16627  isprm3  16730  isprm5  16754  isprm7  16755  xpsfrnel  17622  isacs2  17711  isfull2  17978  isfth2  17982  tosso  18489  odudlatb  18595  ismhm0  18825  issubmndb  18840  nsgacs  19202  isgim2  19305  isabl2  19832  iscyg3  19928  iscrng2  20279  isrnghmmul  20468  isrim  20518  isnzr2  20544  0ringdif  20553  isdomn6  20736  isdomn3  20737  isdrng2  20765  drngprop  20766  issdrg2  20818  islmim2  21088  islpir2  21363  iunocv  21722  ishil2  21762  islinds2  21856  ssntr  23087  isclo2  23117  isperf2  23181  isperf3  23182  nrmsep3  23384  isconn2  23443  iskgen3  23578  ptpjpre1  23600  tx1cn  23638  tx2cn  23639  hausdiag  23674  qustgplem  24150  istdrg2  24207  isngp2  24631  isngp3  24632  isnvc2  24741  isclmp  25149  iscvs  25179  isncvsngp  25202  ovoliunlem1  25556  ismbl2  25581  i1f1lem  25743  i1fres  25760  itg1climres  25769  pilem1  26513  ellogrn  26619  ellogdm  26699  1cubr  26903  atandm  26937  atandm2  26938  atandm3  26939  atandm4  26940  atans2  26992  eldmgm  27083  madeval2  27910  elnns2  28362  elzs2  28403  elznns  28406  isfusgrcl  29356  nbgrel  29375  iscusgrvtx  29456  iscusgredg  29458  clwlkclwwlkflem  30036  isph  30854  h2hcau  31011  h2hlm  31012  issh2  31241  isch2  31255  h1dei  31582  elbdop2  31903  dfadj2  31917  cnvadj  31924  hhcno  31936  hhcnf  31937  eleigvec2  31990  riesz2  32098  rnbra  32139  elat2  32372  ofpreima  32683  mpomptxf  32695  f1od2  32735  maprnin  32745  xrofsup  32774  xrdifh  32785  prmidl0  33443  cmpcref  33796  ofcfval  34062  ispisys2  34117  1stmbfm  34225  2ndmbfm  34226  eulerpartlems  34325  eulerpartlemgc  34327  eulerpartlemv  34329  eulerpartlemd  34331  eulerpartlemr  34339  eulerpartlemn  34346  ballotlemodife  34462  sgn3da  34506  oddprm2  34632  bnj945  34749  bnj1172  34977  bnj1296  34997  snmlval  35299  rexxfr3dALT  35607  eldm3  35723  brtxp2  35845  brpprod3a  35850  dffun10  35878  elfuns  35879  brimg  35901  dfrdg4  35915  ellines  36116  opnrebl  36286  bj-ax12ig  36602  bj-equsexval  36626  bj-substw  36688  bj-csbsnlem  36869  bj-clel3gALT  37014  bj-mpomptALT  37085  bj-elid6  37136  bj-eldiag  37142  bj-imdiridlem  37151  bj-imdirco  37156  bj-isrvec  37260  taupilem3  37285  topdifinffinlem  37313  relowlssretop  37329  wl-dfclab  37550  istotbnd3  37731  isbnd2  37743  isbnd3b  37745  exidcl  37836  isdrngo2  37918  isdrngo3  37919  iscrngo2  37957  isdmn2  38015  isfldidl2  38029  isdmn3  38034  brres2  38224  eldmqsres  38243  brxrn2  38331  petlem  38768  islshpat  38973  iscvlat2N  39280  ishlat3N  39310  snatpsubN  39707  diclspsn  41151  reelznn0nn  42425  prjspeclsp  42567  isnacs2  42662  islnm2  43035  islnr2  43071  islnr3  43072  dflim7  43235  omge2  43260  minregex  43496  iscard5  43498  en2pr  43509  pren2  43515  elinintab  43537  elmapintab  43558  elinlem  43560  cnvcnvintabd  43562  sqrtcvallem1  43593  reabsifpos  43596  k0004lem1  44109  2reu8  47027  dfdfat2  47043  prproropf1olem0  47376  prprelb  47390  prprspr2  47392  isodd2  47509  iseven5  47538  isodd7  47539  oddprmne2  47589  clnbgrel  47701  sclnbgrelself  47720  dfvopnbgr2  47725  sgrp2sgrp  47951  eliunxp2  48058  mpomptx2  48059  elbigo  48285  opndisj  48582  isnrm4  48610  iscnrm3  48632  iscnrm4  48634  catprs  48678