Theorem pm5.32i 584

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  pm5.32ri  585  anbi2i  634  anabs5  675  abai  838  annotanannot  847  pm5.33  848  cases  1058  equsexALT  2451  2sb5rf  2504  2eu8  2686  eq2tri  2825  rexbiia  3110  rmobiia  3375  reubiia  3376  rabbiia  3420  ceqsrexbv  3616  euxfrw  3685  euxfr  3687  2reu5  3722  dfpss3  4044  eldifpr  4625  eldiftp  4654  eldifsn  4754  elrint  4955  elriin  5048  rabxp  5711  copsex2gb  5795  eliunxp  5825  dfres3  5985  restidsing  6057  ressn  6288  dflim2  6421  fncnv  6611  dff1o5  6832  respreima  7063  dff4  7098  dffo3  7099  dffo3f  7103  f1ompt  7108  fsn  7133  fconst3  7213  fconst4  7214  eufnfv  7229  dff13  7254  f1mpt  7261  isocnv3  7332  isores2  7333  isoini  7338  eloprabga  7521  mpomptx  7525  resoprab  7530  elrnmpores  7550  ov6g  7576  dfwe2  7774  dflim3  7844  dflim4  7845  dfopab2  8050  dfoprab3s  8051  dfoprab3  8052  fparlem1  8108  fparlem2  8109  fsplit  8113  brtpos2  8229  dftpos3  8241  tpostpos  8243  dfsmo2  8335  dfrecs3  8360  tz7.48-1  8431  ondif1  8487  ondif2  8488  elixp2  8900  xpcomco  9056  pssnn  9154  enfi  9172  eqinf  9446  infempty  9470  ttrclselem2  9696  frr2  9733  r0weon  9997  isinfcard  10077  dfac5lem1  10108  fpwwe  10632  axgroth6  10814  axgroth3  10817  elni2  10863  indpi  10893  recmulnq  10950  genpass  10995  lemul1a  12070  sup3  12173  elnn0z  12605  elznn0  12607  elznn  12608  eluz2b1  12944  eluz2b3  12947  elfz2nn0  13648  elfzo3  13707  shftidt2  15120  sgn3da  15140  clim0  15559  fprod2dlem  16036  divalglem4  16455  ndvdsadd  16469  gcdaddmlem  16583  algfx  16639  isprm3  16742  isprm5  16767  isprm7  16768  xpsfrnel  17617  isacs2  17710  isfull2  17971  isfth2  17975  tosso  18474  odudlatb  18582  ismhm0  18849  issubmndb  18864  nsgacs  19229  isgim2  19336  isabl2  19861  iscyg3  19957  iscrng2  20335  isrnghmmul  20525  isrim  20575  isnzr2  20602  0ringdif  20612  isdomn6  20799  isdomn3  20800  isdrng2  20830  drngprop  20831  issdrg2  20879  islmim2  21168  isfieldidl  21367  isfieldidl2  21368  prmidl0  21459  islpir2  21479  iunocv  21812  ishil2  21850  islinds2  21944  ssntr  23196  isclo2  23226  isperf2  23290  isperf3  23291  nrmsep3  23493  isconn2  23552  iskgen3  23687  ptpjpre1  23709  tx1cn  23747  tx2cn  23748  hausdiag  23783  qustgplem  24259  istdrg2  24316  isngp2  24735  isngp3  24736  isnvc2  24837  isclmp  25237  iscvs  25267  isncvsngp  25289  ovoliunlem1  25642  ismbl2  25667  i1f1lem  25829  i1fres  25845  itg1climres  25854  pilem1  26592  ellogrn  26702  ellogdm  26782  1cubr  26985  atandm  27019  atandm2  27020  atandm3  27021  atandm4  27022  atans2  27074  eldmgm  27164  madeval2  28004  elnns2  28512  elzs2  28570  elznns  28573  elreno2  28666  isfusgrcl  29649  nbgrel  29668  iscusgrvtx  29749  iscusgredg  29751  dfpth2  30056  clwlkclwwlkflem  30333  isph  31152  h2hcau  31309  h2hlm  31310  issh2  31539  isch2  31553  h1dei  31880  elbdop2  32201  dfadj2  32215  cnvadj  32222  hhcno  32234  hhcnf  32235  eleigvec2  32288  riesz2  32396  rnbra  32437  elat2  32670  ofpreima  32988  mpomptxf  33001  f1od2  33042  maprnin  33054  xrofsup  33090  xrdifh  33103  cmpcref  34218  ofcfval  34466  ispisys2  34521  1stmbfm  34628  2ndmbfm  34629  eulerpartlems  34728  eulerpartlemgc  34730  eulerpartlemv  34732  eulerpartlemd  34734  eulerpartlemr  34742  eulerpartlemn  34749  ballotlemodife  34866  oddprm2  35020  bnj945  35140  bnj1172  35367  bnj1296  35387  snmlval  35801  rexxfr3dALT  36109  eldm3  36231  brtxp2  36349  brpprod3a  36354  dffun10  36382  elfuns  36383  brimg  36405  dfrdg4  36421  ellines  36622  opnrebl  36809  mh-regprimbi  37034  bj-ax12ig  37221  bj-equsexval  37260  bj-substw  37328  bj-csbsnlem  37516  bj-clel3gALT  37662  bj-mpomptALT  37739  bj-elid6  37792  bj-eldiag  37798  bj-imdiridlem  37807  bj-imdirco  37812  bj-isrvec  37916  taupilem3  37941  topdifinffinlem  37971  relowlssretop  37987  wl-dfclab  38218  istotbnd3  38400  isbnd2  38412  isbnd3b  38414  exidcl  38505  isdrngo2  38587  isdrngo3  38588  iscrngo2  38626  isdmn2  38684  isfldidl2  38698  isdmn3  38703  brres2  38900  eldmqsres  38920  brxrn2  39011  blockadjliftmap  39085  qmapeldisjsim  39487  petlem  39542  eldisjs7  39568  petseq  39603  islshpat  39769  iscvlat2N  40076  ishlat3N  40106  snatpsubN  40502  diclspsn  41946  redvmptabs  43099  reelznn0nn  43213  prjspeclsp  43324  isnacs2  43417  islnm2  43785  islnr2  43821  islnr3  43822  dflim7  43980  omge2  44005  minregex  44240  iscard5  44242  en2pr  44253  pren2  44259  elinintab  44281  elmapintab  44302  elinlem  44304  cnvcnvintabd  44306  sqrtcvallem1  44337  reabsifpos  44340  k0004lem1  44853  2reu8  47826  dfdfat2  47842  prproropf1olem0  48228  prprelb  48242  prprspr2  48244  isodd2  48377  iseven5  48406  isodd7  48407  oddprmne2  48457  clnbgrel  48570  sclnbgrelself  48590  dfvopnbgr2  48595  sgrp2sgrp  48970  isidom3  49087  eliunxp2  49091  mpomptx2  49092  elbigo  49308  tposres0  49632  opndisj  49658  isnrm4  49686  iscnrm3  49707  iscnrm4  49709  catprs  49766  initopropd  49998  termopropd  49999  zeroopropd  50000  catcsect  50153  2arwcatlem1  50350  setc1onsubc  50357  alsralrex  50567  alsraln0  50568