Theorem pm5.32i 585

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm5.32ri  586  anbi2i  635  anabs5  676  abai  839  annotanannot  848  pm5.33  849  cases  1058  equsexALT  2448  2sb5rf  2501  2eu8  2683  eq2tri  2822  rexbiia  3107  rmobiia  3371  reubiia  3372  rabbiia  3416  ceqsrexbv  3609  euxfrw  3678  euxfr  3680  2reu5  3715  dfpss3  4016  eldifpr  4615  eldiftp  4644  eldifsn  4744  elrint  4948  elriin  5040  rabxp  5698  copsex2gb  5783  eliunxp  5813  dfres3  5974  restidsing  6044  ressn  6288  dflim2  6421  fncnv  6613  dff1o5  6834  respreima  7065  dff4  7101  dffo3  7102  dffo3f  7106  f1ompt  7111  fsn  7136  fconst3  7219  fconst4  7220  eufnfv  7235  dff13  7258  f1mpt  7265  isocnv3  7340  isores2  7341  isoini  7346  eloprabga  7529  mpomptx  7533  resoprab  7538  elrnmpores  7558  ov6g  7584  mpt3mpt  7685  dfwe2  7788  dflim3  7858  dflim4  7859  dfopab2  8063  dfoprab3s  8064  dfoprab3  8065  f1od2  8110  fparlem1  8125  fparlem2  8126  fsplit  8130  brtpos2  8252  dftpos3  8264  tpostpos  8266  dfsmo2  8358  dfrecs3  8383  tz7.48-1  8456  ondif1  8512  ondif2  8513  elixp2  8932  xpcomco  9089  pssnn  9187  enfi  9205  eqinf  9480  infempty  9504  ttrclselem2  9730  frr2  9767  r0weon  10094  isinfcard  10174  dfac5lem1  10205  fpwwe  10734  axgroth6  10916  axgroth3  10919  elni2  10965  indpi  10995  recmulnq  11052  genpass  11097  lemul1a  12174  sup3  12277  elnn0z  12709  elznn0  12711  elznn  12712  eluz2b1  13049  eluz2b3  13052  elfz2nn0  13755  elfzo3  13814  shftidt2  15239  sgn3da  15259  clim0  15678  fprod2dlem  16152  divalglem4  16571  ndvdsadd  16585  gcdaddmlem  16701  algfx  16760  isprm3  16863  isprm5  16888  isprm7  16889  xpsfrnel  17739  isacs2  17832  isfull2  18093  isfth2  18097  tosso  18596  odudlatb  18704  ismhm0  18990  issubmndb  19005  nsgacs  19377  isgim2  19484  isabl2  20009  iscyg3  20105  iscrng2  20484  isrnghmmul  20677  isrim  20733  isnzr2  20773  0ringdif  20783  isdomn6  20970  isdomn3  20971  drngprop  21003  isdrng3  21012  isdrng5  21013  issdrg2  21057  islmim2  21346  isfieldidl  21545  isfieldidl2  21546  prmidl0  21639  islpir2  21659  iunocv  21992  ishil2  22030  islinds2  22124  ssntr  23381  isclo2  23411  isperf2  23475  isperf3  23476  nrmsep3  23678  isconn2  23737  iskgen3  23873  ptpjpre1  23895  tx1cn  23933  tx2cn  23934  hausdiag  23969  qustgplem  24445  istdrg2  24502  isngp2  24921  isngp3  24922  isnvc2  25023  isclmp  25423  iscvs  25453  isncvsngp  25475  ovoliunlem1  25828  ismbl2  25853  i1f1lem  26015  i1fres  26031  itg1climres  26040  pilem1  26783  ellogrn  26892  ellogdm  26972  1cubr  27175  atandm  27209  atandm2  27210  atandm3  27211  atandm4  27212  atans2  27264  eldmgm  27354  madeval2  28224  elnns2  28732  elzs2  28790  elznns  28793  elreno2  28886  isfusgrcl  29907  nbgrel  29926  iscusgrvtx  30007  iscusgredg  30009  dfpth2  30319  clwlkclwwlkflem  30600  isph  31429  h2hcau  31586  h2hlm  31587  issh2  31816  isch2  31830  h1dei  32157  elbdop2  32478  dfadj2  32492  cnvadj  32499  hhcno  32511  hhcnf  32512  eleigvec2  32565  riesz2  32673  rnbra  32714  elat2  32947  ofpreima  33306  mpomptxf  33319  maprnin  33369  xrofsup  33405  xrdifh  33418  cmpcref  34528  ofcfval  34776  ispisys2  34832  1stmbfm  34938  2ndmbfm  34939  eulerpartlems  35038  eulerpartlemgc  35040  eulerpartlemv  35042  eulerpartlemd  35044  eulerpartlemr  35052  eulerpartlemn  35059  ballotlemodife  35176  oddprm2  35330  bnj945  35450  bnj1172  35677  bnj1296  35697  snmlval  36182  rexxfr3dALT  36490  eldm3  36618  brtxp2  36735  brpprod3a  36740  dffun10  36768  elfuns  36769  brimg  36791  dfrdg4  36807  ellines  37009  opnrebl  37200  mh-regprimbi  37425  bj-ax12ig  37612  bj-equsexval  37651  bj-substw  37719  bj-csbsnlem  37907  coi1in  38053  bj-clel3gALT  38055  bj-mpomptALT  38133  bj-elid6  38184  bj-eldiag  38190  bj-imdiridlem  38199  bj-imdirco  38204  bj-isrvec  38308  taupilem3  38333  topdifinffinlem  38363  relowlssretop  38379  wl-dfclab  38610  istotbnd3  38798  isbnd2  38810  isbnd3b  38812  exidcl  38903  isdrngo2  38985  isdrngo3  38986  iscrngo2  39024  isdmn2  39082  isfldidl2  39096  isdmn3  39101  brres2  39298  eldmqsres  39318  brxrn2  39409  blockadjliftmap  39483  qmapeldisjsim  39885  petlem  39940  eldisjs7  39966  petseq  40001  islshpat  40167  iscvlat2N  40474  ishlat3N  40504  snatpsubN  40900  diclspsn  42344  redvmptabs  43504  reelznn0nn  43618  prjspeclsp  43733  isnacs2  43810  islnm2  44173  islnr2  44209  islnr3  44210  dflim7  44368  omge2  44393  minregex  44628  iscard5  44630  en2pr  44641  pren2  44647  elinintab  44669  elmapintab  44689  elinlem  44691  cnvcnvintabd  44693  sqrtcvallem1  44724  reabsifpos  44727  k0004lem1  45240  2reu8  48275  dfdfat2  48291  prproropf1olem0  48677  prprelb  48691  prprspr2  48693  isodd2  48826  iseven5  48855  isodd7  48856  oddprmne2  48906  clnbgrel  49019  sclnbgrelself  49039  dfvopnbgr2  49044  sgrp2sgrp  49418  isidom3  49535  eliunxp2  49539  mpomptx2  49540  elbigo  49756  rrx2xpref1o  49924  tposres0  50083  opndisj  50110  isnrm4  50138  iscnrm3  50159  iscnrm4  50161  catprs  50218  initopropd  50458  termopropd  50459  zeroopropd  50460  catcsect  50626  2arwcatlem1  50826  setc1onsubc  50833  alsralrex  51076  alsraln0  51077  dfalseu2  51100