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  624  anabs5  664  abai  827  annotanannot  835  pm5.33  836  cases  1043  equsexALT  2424  2sb5rf  2477  2eu8  2660  eq2tri  2799  rexbiia  3083  rmobiia  3358  reubiia  3359  rabbiia  3405  ceqsrexbv  3612  euxfrw  3681  euxfr  3683  2reu5  3718  dfpss3  4043  eldifpr  4617  eldiftp  4646  eldifsn  4744  elrint  4946  elriin  5038  rabxp  5680  copsex2gb  5763  eliunxp  5794  dfres3  5951  restidsing  6020  ressn  6251  dflim2  6383  fncnv  6573  dff1o5  6791  respreima  7020  dff4  7055  dffo3  7056  dffo3f  7060  f1ompt  7065  fsn  7090  fconst3  7169  fconst4  7170  eufnfv  7185  dff13  7210  f1mpt  7217  isocnv3  7288  isores2  7289  isoini  7294  eloprabga  7477  mpomptx  7481  resoprab  7486  elrnmpores  7506  ov6g  7532  dfwe2  7729  dflim3  7799  dflim4  7800  dfopab2  8006  dfoprab3s  8007  dfoprab3  8008  fparlem1  8064  fparlem2  8065  fsplit  8069  brtpos2  8184  dftpos3  8196  tpostpos  8198  dfsmo2  8289  dfrecs3  8314  tz7.48-1  8384  ondif1  8438  ondif2  8439  elixp2  8851  xpcomco  9007  pssnn  9105  enfi  9123  eqinf  9400  infempty  9424  ttrclselem2  9647  frr2  9684  r0weon  9934  isinfcard  10014  dfac5lem1  10045  fpwwe  10569  axgroth6  10751  axgroth3  10754  elni2  10800  indpi  10830  recmulnq  10887  genpass  10932  lemul1a  12007  sup3  12111  elnn0z  12513  elznn0  12515  elznn  12516  eluz2b1  12844  eluz2b3  12847  elfz2nn0  13546  elfzo3  13604  shftidt2  15016  clim0  15441  fprod2dlem  15915  divalglem4  16335  ndvdsadd  16349  gcdaddmlem  16463  algfx  16519  isprm3  16622  isprm5  16646  isprm7  16647  xpsfrnel  17495  isacs2  17588  isfull2  17849  isfth2  17853  tosso  18352  odudlatb  18460  ismhm0  18727  issubmndb  18742  nsgacs  19103  isgim2  19206  isabl2  19731  iscyg3  19827  iscrng2  20199  isrnghmmul  20390  isrim  20439  isnzr2  20463  0ringdif  20472  isdomn6  20659  isdomn3  20660  isdrng2  20688  drngprop  20689  issdrg2  20740  islmim2  21030  islpir2  21297  iunocv  21648  ishil2  21686  islinds2  21780  ssntr  23014  isclo2  23044  isperf2  23108  isperf3  23109  nrmsep3  23311  isconn2  23370  iskgen3  23505  ptpjpre1  23527  tx1cn  23565  tx2cn  23566  hausdiag  23601  qustgplem  24077  istdrg2  24134  isngp2  24553  isngp3  24554  isnvc2  24655  isclmp  25065  iscvs  25095  isncvsngp  25117  ovoliunlem1  25471  ismbl2  25496  i1f1lem  25658  i1fres  25674  itg1climres  25683  pilem1  26429  ellogrn  26536  ellogdm  26616  1cubr  26820  atandm  26854  atandm2  26855  atandm3  26856  atandm4  26857  atans2  26909  eldmgm  27000  madeval2  27841  elnns2  28349  elzs2  28407  elznns  28410  elreno2  28503  isfusgrcl  29406  nbgrel  29425  iscusgrvtx  29506  iscusgredg  29508  dfpth2  29814  clwlkclwwlkflem  30091  isph  30909  h2hcau  31066  h2hlm  31067  issh2  31296  isch2  31310  h1dei  31637  elbdop2  31958  dfadj2  31972  cnvadj  31979  hhcno  31991  hhcnf  31992  eleigvec2  32045  riesz2  32153  rnbra  32194  elat2  32427  ofpreima  32754  mpomptxf  32767  f1od2  32808  maprnin  32820  xrofsup  32857  xrdifh  32870  sgn3da  32925  prmidl0  33542  cmpcref  34027  ofcfval  34275  ispisys2  34330  1stmbfm  34437  2ndmbfm  34438  eulerpartlems  34537  eulerpartlemgc  34539  eulerpartlemv  34541  eulerpartlemd  34543  eulerpartlemr  34551  eulerpartlemn  34558  ballotlemodife  34675  oddprm2  34832  bnj945  34949  bnj1172  35176  bnj1296  35196  snmlval  35544  rexxfr3dALT  35852  eldm3  35974  brtxp2  36092  brpprod3a  36097  dffun10  36125  elfuns  36126  brimg  36148  dfrdg4  36164  ellines  36365  opnrebl  36533  bj-ax12ig  36866  bj-equsexval  36899  bj-substw  36962  bj-csbsnlem  37145  bj-clel3gALT  37290  bj-mpomptALT  37366  bj-elid6  37419  bj-eldiag  37425  bj-imdiridlem  37434  bj-imdirco  37439  bj-isrvec  37543  taupilem3  37568  topdifinffinlem  37596  relowlssretop  37612  wl-dfclab  37834  istotbnd3  38016  isbnd2  38028  isbnd3b  38030  exidcl  38121  isdrngo2  38203  isdrngo3  38204  iscrngo2  38242  isdmn2  38300  isfldidl2  38314  isdmn3  38319  brres2  38518  eldmqsres  38538  brxrn2  38629  blockadjliftmap  38703  qmapeldisjsim  39105  petlem  39160  eldisjs7  39186  petseq  39221  islshpat  39387  iscvlat2N  39694  ishlat3N  39724  snatpsubN  40120  diclspsn  41564  redvmptabs  42724  reelznn0nn  42825  prjspeclsp  42964  isnacs2  43057  islnm2  43429  islnr2  43465  islnr3  43466  dflim7  43624  omge2  43649  minregex  43884  iscard5  43886  en2pr  43897  pren2  43903  elinintab  43925  elmapintab  43946  elinlem  43948  cnvcnvintabd  43950  sqrtcvallem1  43981  reabsifpos  43984  k0004lem1  44497  2reu8  47466  dfdfat2  47482  prproropf1olem0  47856  prprelb  47870  prprspr2  47872  isodd2  47989  iseven5  48018  isodd7  48019  oddprmne2  48069  clnbgrel  48182  sclnbgrelself  48202  dfvopnbgr2  48207  sgrp2sgrp  48582  eliunxp2  48688  mpomptx2  48689  elbigo  48905  tposres0  49230  opndisj  49256  isnrm4  49284  iscnrm3  49305  iscnrm4  49307  catprs  49364  initopropd  49596  termopropd  49597  zeroopropd  49598  catcsect  49751  2arwcatlem1  49948  setc1onsubc  49955