Theorem pm5.32i 579

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm5.32ri  580  anbi2i  629  anabs5  669  abai  832  annotanannot  840  pm5.33  841  cases  1048  equsexALT  2427  2sb5rf  2480  2eu8  2663  eq2tri  2802  rexbiia  3085  rmobiia  3351  reubiia  3352  rabbiia  3396  ceqsrexbv  3601  euxfrw  3669  euxfr  3671  2reu5  3706  dfpss3  4027  eldifpr  4597  eldiftp  4626  eldifsn  4726  elrint  4926  elriin  5017  rabxp  5673  copsex2gb  5756  eliunxp  5786  dfres3  5943  restidsing  6012  ressn  6243  dflim2  6375  fncnv  6565  dff1o5  6783  respreima  7014  dff4  7049  dffo3  7050  dffo3f  7054  f1ompt  7059  fsn  7084  fconst3  7164  fconst4  7165  eufnfv  7180  dff13  7205  f1mpt  7212  isocnv3  7283  isores2  7284  isoini  7289  eloprabga  7472  mpomptx  7476  resoprab  7481  elrnmpores  7501  ov6g  7527  dfwe2  7724  dflim3  7794  dflim4  7795  dfopab2  8001  dfoprab3s  8002  dfoprab3  8003  fparlem1  8058  fparlem2  8059  fsplit  8063  brtpos2  8179  dftpos3  8191  tpostpos  8193  dfsmo2  8284  dfrecs3  8309  tz7.48-1  8379  ondif1  8433  ondif2  8434  elixp2  8846  xpcomco  9002  pssnn  9100  enfi  9118  eqinf  9395  infempty  9419  ttrclselem2  9645  frr2  9682  r0weon  9932  isinfcard  10012  dfac5lem1  10043  fpwwe  10567  axgroth6  10749  axgroth3  10752  elni2  10798  indpi  10828  recmulnq  10885  genpass  10930  lemul1a  12007  sup3  12111  elnn0z  12535  elznn0  12537  elznn  12538  eluz2b1  12867  eluz2b3  12870  elfz2nn0  13570  elfzo3  13629  shftidt2  15041  clim0  15466  fprod2dlem  15943  divalglem4  16363  ndvdsadd  16377  gcdaddmlem  16491  algfx  16547  isprm3  16650  isprm5  16675  isprm7  16676  xpsfrnel  17524  isacs2  17617  isfull2  17878  isfth2  17882  tosso  18381  odudlatb  18489  ismhm0  18756  issubmndb  18771  nsgacs  19135  isgim2  19238  isabl2  19763  iscyg3  19859  iscrng2  20231  isrnghmmul  20420  isrim  20470  isnzr2  20497  0ringdif  20506  isdomn6  20693  isdomn3  20694  isdrng2  20722  drngprop  20723  issdrg2  20774  islmim2  21063  islpir2  21330  iunocv  21663  ishil2  21701  islinds2  21795  ssntr  23048  isclo2  23078  isperf2  23142  isperf3  23143  nrmsep3  23345  isconn2  23404  iskgen3  23539  ptpjpre1  23561  tx1cn  23599  tx2cn  23600  hausdiag  23635  qustgplem  24111  istdrg2  24168  isngp2  24587  isngp3  24588  isnvc2  24689  isclmp  25089  iscvs  25119  isncvsngp  25141  ovoliunlem1  25494  ismbl2  25519  i1f1lem  25681  i1fres  25697  itg1climres  25706  pilem1  26441  ellogrn  26548  ellogdm  26628  1cubr  26831  atandm  26865  atandm2  26866  atandm3  26867  atandm4  26868  atans2  26920  eldmgm  27010  madeval2  27850  elnns2  28358  elzs2  28416  elznns  28419  elreno2  28512  isfusgrcl  29415  nbgrel  29434  iscusgrvtx  29515  iscusgredg  29517  dfpth2  29822  clwlkclwwlkflem  30099  isph  30918  h2hcau  31075  h2hlm  31076  issh2  31305  isch2  31319  h1dei  31646  elbdop2  31967  dfadj2  31981  cnvadj  31988  hhcno  32000  hhcnf  32001  eleigvec2  32054  riesz2  32162  rnbra  32203  elat2  32436  ofpreima  32764  mpomptxf  32777  f1od2  32818  maprnin  32830  xrofsup  32866  xrdifh  32879  sgn3da  32933  prmidl0  33540  cmpcref  34041  ofcfval  34289  ispisys2  34344  1stmbfm  34451  2ndmbfm  34452  eulerpartlems  34551  eulerpartlemgc  34553  eulerpartlemv  34555  eulerpartlemd  34557  eulerpartlemr  34565  eulerpartlemn  34572  ballotlemodife  34689  oddprm2  34846  bnj945  34963  bnj1172  35190  bnj1296  35210  snmlval  35566  rexxfr3dALT  35874  eldm3  35996  brtxp2  36114  brpprod3a  36119  dffun10  36147  elfuns  36148  brimg  36170  dfrdg4  36186  ellines  36387  opnrebl  36555  mh-regprimbi  36780  bj-ax12ig  36968  bj-equsexval  37007  bj-substw  37075  bj-csbsnlem  37263  bj-clel3gALT  37408  bj-mpomptALT  37484  bj-elid6  37537  bj-eldiag  37543  bj-imdiridlem  37552  bj-imdirco  37557  bj-isrvec  37661  taupilem3  37686  topdifinffinlem  37716  relowlssretop  37732  wl-dfclab  37963  istotbnd3  38145  isbnd2  38157  isbnd3b  38159  exidcl  38250  isdrngo2  38332  isdrngo3  38333  iscrngo2  38371  isdmn2  38429  isfldidl2  38443  isdmn3  38448  brres2  38647  eldmqsres  38667  brxrn2  38758  blockadjliftmap  38832  qmapeldisjsim  39234  petlem  39289  eldisjs7  39315  petseq  39350  islshpat  39516  iscvlat2N  39823  ishlat3N  39853  snatpsubN  40249  diclspsn  41693  redvmptabs  42844  reelznn0nn  42958  prjspeclsp  43069  isnacs2  43162  islnm2  43530  islnr2  43566  islnr3  43567  dflim7  43725  omge2  43750  minregex  43985  iscard5  43987  en2pr  43998  pren2  44004  elinintab  44026  elmapintab  44047  elinlem  44049  cnvcnvintabd  44051  sqrtcvallem1  44082  reabsifpos  44085  k0004lem1  44598  2reu8  47582  dfdfat2  47598  prproropf1olem0  47984  prprelb  47998  prprspr2  48000  isodd2  48133  iseven5  48162  isodd7  48163  oddprmne2  48213  clnbgrel  48326  sclnbgrelself  48346  dfvopnbgr2  48351  sgrp2sgrp  48726  eliunxp2  48832  mpomptx2  48833  elbigo  49049  tposres0  49374  opndisj  49400  isnrm4  49428  iscnrm3  49449  iscnrm4  49451  catprs  49508  initopropd  49740  termopropd  49741  zeroopropd  49742  catcsect  49895  2arwcatlem1  50092  setc1onsubc  50099