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  826  annotanannot  834  pm5.33  835  cases  1042  equsexALT  2421  2sb5rf  2474  2eu8  2656  eq2tri  2795  rexbiia  3078  rmobiia  3353  reubiia  3354  rabbiia  3400  ceqsrexbv  3607  euxfrw  3676  euxfr  3678  2reu5  3713  dfpss3  4038  eldifpr  4610  eldiftp  4639  eldifsn  4737  elrint  4939  elriin  5031  rabxp  5667  copsex2gb  5750  eliunxp  5781  dfres3  5937  restidsing  6006  ressn  6237  dflim2  6369  fncnv  6559  dff1o5  6777  respreima  7005  dff4  7040  dffo3  7041  dffo3f  7045  f1ompt  7050  fsn  7074  fconst3  7153  fconst4  7154  eufnfv  7169  dff13  7194  f1mpt  7201  isocnv3  7272  isores2  7273  isoini  7278  eloprabga  7461  mpomptx  7465  resoprab  7470  elrnmpores  7490  ov6g  7516  dfwe2  7713  dflim3  7783  dflim4  7784  dfopab2  7990  dfoprab3s  7991  dfoprab3  7992  fparlem1  8048  fparlem2  8049  fsplit  8053  brtpos2  8168  dftpos3  8180  tpostpos  8182  dfsmo2  8273  dfrecs3  8298  tz7.48-1  8368  ondif1  8422  ondif2  8423  elixp2  8831  xpcomco  8987  pssnn  9085  enfi  9103  eqinf  9376  infempty  9400  ttrclselem2  9623  frr2  9660  r0weon  9910  isinfcard  9990  dfac5lem1  10021  fpwwe  10544  axgroth6  10726  axgroth3  10729  elni2  10775  indpi  10805  recmulnq  10862  genpass  10907  lemul1a  11982  sup3  12086  elnn0z  12488  elznn0  12490  elznn  12491  eluz2b1  12819  eluz2b3  12822  elfz2nn0  13520  elfzo3  13578  shftidt2  14990  clim0  15415  fprod2dlem  15889  divalglem4  16309  ndvdsadd  16323  gcdaddmlem  16437  algfx  16493  isprm3  16596  isprm5  16620  isprm7  16621  xpsfrnel  17468  isacs2  17561  isfull2  17822  isfth2  17826  tosso  18325  odudlatb  18433  ismhm0  18700  issubmndb  18715  nsgacs  19076  isgim2  19179  isabl2  19704  iscyg3  19800  iscrng2  20172  isrnghmmul  20362  isrim  20411  isnzr2  20435  0ringdif  20444  isdomn6  20631  isdomn3  20632  isdrng2  20660  drngprop  20661  issdrg2  20712  islmim2  21002  islpir2  21269  iunocv  21620  ishil2  21658  islinds2  21752  ssntr  22974  isclo2  23004  isperf2  23068  isperf3  23069  nrmsep3  23271  isconn2  23330  iskgen3  23465  ptpjpre1  23487  tx1cn  23525  tx2cn  23526  hausdiag  23561  qustgplem  24037  istdrg2  24094  isngp2  24513  isngp3  24514  isnvc2  24615  isclmp  25025  iscvs  25055  isncvsngp  25077  ovoliunlem1  25431  ismbl2  25456  i1f1lem  25618  i1fres  25634  itg1climres  25643  pilem1  26389  ellogrn  26496  ellogdm  26576  1cubr  26780  atandm  26814  atandm2  26815  atandm3  26816  atandm4  26817  atans2  26869  eldmgm  26960  madeval2  27795  elnns2  28270  elzs2  28324  elznns  28327  isfusgrcl  29301  nbgrel  29320  iscusgrvtx  29401  iscusgredg  29403  dfpth2  29709  clwlkclwwlkflem  29986  isph  30804  h2hcau  30961  h2hlm  30962  issh2  31191  isch2  31205  h1dei  31532  elbdop2  31853  dfadj2  31867  cnvadj  31874  hhcno  31886  hhcnf  31887  eleigvec2  31940  riesz2  32048  rnbra  32089  elat2  32322  ofpreima  32649  mpomptxf  32663  f1od2  32706  maprnin  32718  xrofsup  32754  xrdifh  32767  sgn3da  32822  prmidl0  33422  cmpcref  33884  ofcfval  34132  ispisys2  34187  1stmbfm  34294  2ndmbfm  34295  eulerpartlems  34394  eulerpartlemgc  34396  eulerpartlemv  34398  eulerpartlemd  34400  eulerpartlemr  34408  eulerpartlemn  34415  ballotlemodife  34532  oddprm2  34689  bnj945  34806  bnj1172  35034  bnj1296  35054  snmlval  35396  rexxfr3dALT  35704  eldm3  35826  brtxp2  35944  brpprod3a  35949  dffun10  35977  elfuns  35978  brimg  36000  dfrdg4  36016  ellines  36217  opnrebl  36385  bj-ax12ig  36701  bj-equsexval  36725  bj-substw  36787  bj-csbsnlem  36968  bj-clel3gALT  37113  bj-mpomptALT  37184  bj-elid6  37235  bj-eldiag  37241  bj-imdiridlem  37250  bj-imdirco  37255  bj-isrvec  37359  taupilem3  37384  topdifinffinlem  37412  relowlssretop  37428  wl-dfclab  37650  istotbnd3  37831  isbnd2  37843  isbnd3b  37845  exidcl  37936  isdrngo2  38018  isdrngo3  38019  iscrngo2  38057  isdmn2  38115  isfldidl2  38129  isdmn3  38134  brres2  38325  eldmqsres  38345  brxrn2  38428  blockadjliftmap  38492  petlem  38930  islshpat  39136  iscvlat2N  39443  ishlat3N  39473  snatpsubN  39869  diclspsn  41313  redvmptabs  42478  reelznn0nn  42579  prjspeclsp  42730  isnacs2  42823  islnm2  43195  islnr2  43231  islnr3  43232  dflim7  43390  omge2  43415  minregex  43651  iscard5  43653  en2pr  43664  pren2  43670  elinintab  43692  elmapintab  43713  elinlem  43715  cnvcnvintabd  43717  sqrtcvallem1  43748  reabsifpos  43751  k0004lem1  44264  2reu8  47236  dfdfat2  47252  prproropf1olem0  47626  prprelb  47640  prprspr2  47642  isodd2  47759  iseven5  47788  isodd7  47789  oddprmne2  47839  clnbgrel  47952  sclnbgrelself  47972  dfvopnbgr2  47977  sgrp2sgrp  48352  eliunxp2  48458  mpomptx2  48459  elbigo  48676  tposres0  49001  opndisj  49027  isnrm4  49055  iscnrm3  49076  iscnrm4  49078  catprs  49136  initopropd  49368  termopropd  49369  zeroopropd  49370  catcsect  49523  2arwcatlem1  49720  setc1onsubc  49727