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  2454  2sb5rf  2507  2eu8  2689  eq2tri  2828  rexbiia  3113  rmobiia  3378  reubiia  3379  rabbiia  3423  ceqsrexbv  3618  euxfrw  3687  euxfr  3689  2reu5  3724  dfpss3  4046  eldifpr  4629  eldiftp  4658  eldifsn  4758  elrint  4959  elriin  5052  rabxp  5714  copsex2gb  5798  eliunxp  5828  dfres3  5988  restidsing  6060  ressn  6293  dflim2  6426  fncnv  6616  dff1o5  6837  respreima  7068  dff4  7103  dffo3  7104  dffo3f  7108  f1ompt  7113  fsn  7138  fconst3  7218  fconst4  7219  eufnfv  7234  dff13  7259  f1mpt  7266  isocnv3  7341  isores2  7342  isoini  7347  eloprabga  7532  mpomptx  7536  resoprab  7541  elrnmpores  7561  ov6g  7587  dfwe2  7782  dflim3  7852  dflim4  7853  dfopab2  8058  dfoprab3s  8059  dfoprab3  8060  fparlem1  8116  fparlem2  8117  fsplit  8121  brtpos2  8237  dftpos3  8249  tpostpos  8251  dfsmo2  8343  dfrecs3  8368  tz7.48-1  8439  ondif1  8495  ondif2  8496  elixp2  8908  xpcomco  9065  pssnn  9163  enfi  9181  eqinf  9455  infempty  9479  ttrclselem2  9705  frr2  9742  r0weon  10015  isinfcard  10095  dfac5lem1  10126  fpwwe  10649  axgroth6  10831  axgroth3  10834  elni2  10880  indpi  10910  recmulnq  10967  genpass  11012  lemul1a  12087  sup3  12190  elnn0z  12622  elznn0  12624  elznn  12625  eluz2b1  12961  eluz2b3  12964  elfz2nn0  13665  elfzo3  13724  shftidt2  15144  sgn3da  15164  clim0  15583  fprod2dlem  16060  divalglem4  16479  ndvdsadd  16493  gcdaddmlem  16607  algfx  16663  isprm3  16766  isprm5  16791  isprm7  16792  xpsfrnel  17641  isacs2  17734  isfull2  17995  isfth2  17999  tosso  18498  odudlatb  18606  ismhm0  18879  issubmndb  18894  nsgacs  19259  isgim2  19366  isabl2  19891  iscyg3  19987  iscrng2  20365  isrnghmmul  20557  isrim  20613  isnzr2  20652  0ringdif  20662  isdomn6  20849  isdomn3  20850  isdrng2  20880  drngprop  20881  isdrng3  20890  isdrng5  20891  issdrg2  20935  islmim2  21224  isfieldidl  21423  isfieldidl2  21424  prmidl0  21515  islpir2  21535  iunocv  21868  ishil2  21906  islinds2  22000  ssntr  23252  isclo2  23282  isperf2  23346  isperf3  23347  nrmsep3  23549  isconn2  23608  iskgen3  23743  ptpjpre1  23765  tx1cn  23803  tx2cn  23804  hausdiag  23839  qustgplem  24315  istdrg2  24372  isngp2  24791  isngp3  24792  isnvc2  24893  isclmp  25293  iscvs  25323  isncvsngp  25345  ovoliunlem1  25698  ismbl2  25723  i1f1lem  25885  i1fres  25901  itg1climres  25910  pilem1  26651  ellogrn  26761  ellogdm  26841  1cubr  27044  atandm  27078  atandm2  27079  atandm3  27080  atandm4  27081  atans2  27133  eldmgm  27223  madeval2  28063  elnns2  28571  elzs2  28629  elznns  28632  elreno2  28725  isfusgrcl  29708  nbgrel  29727  iscusgrvtx  29808  iscusgredg  29810  dfpth2  30115  clwlkclwwlkflem  30392  isph  31211  h2hcau  31368  h2hlm  31369  issh2  31598  isch2  31612  h1dei  31939  elbdop2  32260  dfadj2  32274  cnvadj  32281  hhcno  32293  hhcnf  32294  eleigvec2  32347  riesz2  32455  rnbra  32496  elat2  32729  ofpreima  33047  mpomptxf  33060  f1od2  33101  maprnin  33113  xrofsup  33149  xrdifh  33162  cmpcref  34271  ofcfval  34519  ispisys2  34575  1stmbfm  34682  2ndmbfm  34683  eulerpartlems  34782  eulerpartlemgc  34784  eulerpartlemv  34786  eulerpartlemd  34788  eulerpartlemr  34796  eulerpartlemn  34803  ballotlemodife  34920  oddprm2  35074  bnj945  35194  bnj1172  35421  bnj1296  35441  snmlval  35844  rexxfr3dALT  36152  eldm3  36274  brtxp2  36392  brpprod3a  36397  dffun10  36425  elfuns  36426  brimg  36448  dfrdg4  36464  ellines  36665  opnrebl  36872  mh-regprimbi  37097  bj-ax12ig  37284  bj-equsexval  37323  bj-substw  37391  bj-csbsnlem  37579  bj-clel3gALT  37725  bj-mpomptALT  37802  bj-elid6  37855  bj-eldiag  37861  bj-imdiridlem  37870  bj-imdirco  37875  bj-isrvec  37979  taupilem3  38004  topdifinffinlem  38034  relowlssretop  38050  wl-dfclab  38281  istotbnd3  38463  isbnd2  38475  isbnd3b  38477  exidcl  38568  isdrngo2  38650  isdrngo3  38651  iscrngo2  38689  isdmn2  38747  isfldidl2  38761  isdmn3  38766  brres2  38963  eldmqsres  38983  brxrn2  39074  blockadjliftmap  39148  qmapeldisjsim  39550  petlem  39605  eldisjs7  39631  petseq  39666  islshpat  39832  iscvlat2N  40139  ishlat3N  40169  snatpsubN  40565  diclspsn  42009  redvmptabs  43162  reelznn0nn  43276  prjspeclsp  43385  isnacs2  43478  islnm2  43846  islnr2  43882  islnr3  43883  dflim7  44041  omge2  44066  minregex  44301  iscard5  44303  en2pr  44314  pren2  44320  elinintab  44342  elmapintab  44363  elinlem  44365  cnvcnvintabd  44367  sqrtcvallem1  44398  reabsifpos  44401  k0004lem1  44914  2reu8  47890  dfdfat2  47906  prproropf1olem0  48292  prprelb  48306  prprspr2  48308  isodd2  48441  iseven5  48470  isodd7  48471  oddprmne2  48521  clnbgrel  48634  sclnbgrelself  48654  dfvopnbgr2  48659  sgrp2sgrp  49034  isidom3  49151  eliunxp2  49155  mpomptx2  49156  elbigo  49372  tposres0  49696  opndisj  49722  isnrm4  49750  iscnrm3  49771  iscnrm4  49773  catprs  49830  initopropd  50062  termopropd  50063  zeroopropd  50064  catcsect  50217  2arwcatlem1  50414  setc1onsubc  50421  alsralrex  50631  alsraln0  50632  dfalseu2  50655