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  1056  equsexALT  2453  2sb5rf  2506  2eu8  2688  eq2tri  2827  rexbiia  3110  rmobiia  3376  reubiia  3377  rabbiia  3421  ceqsrexbv  3618  euxfrw  3687  euxfr  3689  2reu5  3724  dfpss3  4045  eldifpr  4620  eldiftp  4649  eldifsn  4749  elrint  4950  elriin  5043  rabxp  5700  copsex2gb  5784  eliunxp  5814  dfres3  5974  restidsing  6046  ressn  6276  dflim2  6408  fncnv  6598  dff1o5  6820  respreima  7051  dff4  7086  dffo3  7087  dffo3f  7091  f1ompt  7096  fsn  7121  fconst3  7201  fconst4  7202  eufnfv  7217  dff13  7242  f1mpt  7249  isocnv3  7320  isores2  7321  isoini  7326  eloprabga  7509  mpomptx  7513  resoprab  7518  elrnmpores  7538  ov6g  7564  dfwe2  7761  dflim3  7831  dflim4  7832  dfopab2  8037  dfoprab3s  8038  dfoprab3  8039  fparlem1  8095  fparlem2  8096  fsplit  8100  brtpos2  8216  dftpos3  8228  tpostpos  8230  dfsmo2  8322  dfrecs3  8347  tz7.48-1  8418  ondif1  8474  ondif2  8475  elixp2  8887  xpcomco  9043  pssnn  9141  enfi  9159  eqinf  9433  infempty  9457  ttrclselem2  9683  frr2  9720  r0weon  9984  isinfcard  10064  dfac5lem1  10095  fpwwe  10619  axgroth6  10801  axgroth3  10804  elni2  10850  indpi  10880  recmulnq  10937  genpass  10982  lemul1a  12060  sup3  12163  elnn0z  12595  elznn0  12597  elznn  12598  eluz2b1  12934  eluz2b3  12937  elfz2nn0  13637  elfzo3  13696  shftidt2  15108  sgn3da  15128  clim0  15547  fprod2dlem  16024  divalglem4  16444  ndvdsadd  16458  gcdaddmlem  16572  algfx  16628  isprm3  16731  isprm5  16756  isprm7  16757  xpsfrnel  17606  isacs2  17699  isfull2  17960  isfth2  17964  tosso  18463  odudlatb  18571  ismhm0  18838  issubmndb  18853  nsgacs  19219  isgim2  19326  isabl2  19851  iscyg3  19947  iscrng2  20325  isrnghmmul  20515  isrim  20565  isnzr2  20592  0ringdif  20602  isdomn6  20789  isdomn3  20790  isdrng2  20818  drngprop  20819  issdrg2  20867  islmim2  21156  prmidl0  21438  islpir2  21458  iunocv  21791  ishil2  21829  islinds2  21923  ssntr  23176  isclo2  23206  isperf2  23270  isperf3  23271  nrmsep3  23473  isconn2  23532  iskgen3  23667  ptpjpre1  23689  tx1cn  23727  tx2cn  23728  hausdiag  23763  qustgplem  24239  istdrg2  24296  isngp2  24715  isngp3  24716  isnvc2  24817  isclmp  25217  iscvs  25247  isncvsngp  25269  ovoliunlem1  25622  ismbl2  25647  i1f1lem  25809  i1fres  25825  itg1climres  25834  pilem1  26572  ellogrn  26682  ellogdm  26762  1cubr  26965  atandm  26999  atandm2  27000  atandm3  27001  atandm4  27002  atans2  27054  eldmgm  27144  madeval2  27984  elnns2  28492  elzs2  28550  elznns  28553  elreno2  28646  isfusgrcl  29580  nbgrel  29599  iscusgrvtx  29680  iscusgredg  29682  dfpth2  29987  clwlkclwwlkflem  30264  isph  31083  h2hcau  31240  h2hlm  31241  issh2  31470  isch2  31484  h1dei  31811  elbdop2  32132  dfadj2  32146  cnvadj  32153  hhcno  32165  hhcnf  32166  eleigvec2  32219  riesz2  32327  rnbra  32368  elat2  32601  ofpreima  32922  mpomptxf  32935  f1od2  32976  maprnin  32988  xrofsup  33024  xrdifh  33037  cmpcref  34157  ofcfval  34405  ispisys2  34460  1stmbfm  34567  2ndmbfm  34568  eulerpartlems  34667  eulerpartlemgc  34669  eulerpartlemv  34671  eulerpartlemd  34673  eulerpartlemr  34681  eulerpartlemn  34688  ballotlemodife  34805  oddprm2  34959  bnj945  35079  bnj1172  35306  bnj1296  35326  snmlval  35694  rexxfr3dALT  36002  eldm3  36124  brtxp2  36242  brpprod3a  36247  dffun10  36275  elfuns  36276  brimg  36298  dfrdg4  36314  ellines  36515  opnrebl  36693  mh-regprimbi  36918  bj-ax12ig  37105  bj-equsexval  37144  bj-substw  37212  bj-csbsnlem  37400  bj-clel3gALT  37545  bj-mpomptALT  37621  bj-elid6  37674  bj-eldiag  37680  bj-imdiridlem  37689  bj-imdirco  37694  bj-isrvec  37798  taupilem3  37823  topdifinffinlem  37853  relowlssretop  37869  wl-dfclab  38100  istotbnd3  38282  isbnd2  38294  isbnd3b  38296  exidcl  38387  isdrngo2  38469  isdrngo3  38470  iscrngo2  38508  isdmn2  38566  isfldidl2  38580  isdmn3  38585  brres2  38784  eldmqsres  38804  brxrn2  38895  blockadjliftmap  38969  qmapeldisjsim  39371  petlem  39426  eldisjs7  39452  petseq  39487  islshpat  39653  iscvlat2N  39960  ishlat3N  39990  snatpsubN  40386  diclspsn  41830  redvmptabs  42981  reelznn0nn  43095  prjspeclsp  43206  isnacs2  43299  islnm2  43667  islnr2  43703  islnr3  43704  dflim7  43862  omge2  43887  minregex  44122  iscard5  44124  en2pr  44135  pren2  44141  elinintab  44163  elmapintab  44184  elinlem  44186  cnvcnvintabd  44188  sqrtcvallem1  44219  reabsifpos  44222  k0004lem1  44735  2reu8  47704  dfdfat2  47720  prproropf1olem0  48106  prprelb  48120  prprspr2  48122  isodd2  48255  iseven5  48284  isodd7  48285  oddprmne2  48335  clnbgrel  48448  sclnbgrelself  48468  dfvopnbgr2  48473  sgrp2sgrp  48848  eliunxp2  48965  mpomptx2  48966  elbigo  49182  tposres0  49506  opndisj  49532  isnrm4  49560  iscnrm3  49581  iscnrm4  49583  catprs  49640  initopropd  49872  termopropd  49873  zeroopropd  49874  catcsect  50027  2arwcatlem1  50224  setc1onsubc  50231