Theorem pm5.32i 582

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  pm5.32ri  583  anbi2i  632  anabs5  673  abai  836  annotanannot  845  pm5.33  846  cases  1053  equsexALT  2449  2sb5rf  2502  2eu8  2684  eq2tri  2823  rexbiia  3106  rmobiia  3372  reubiia  3373  rabbiia  3417  ceqsrexbv  3615  euxfrw  3683  euxfr  3685  2reu5  3720  dfpss3  4042  eldifpr  4616  eldiftp  4645  eldifsn  4745  elrint  4946  elriin  5037  rabxp  5693  copsex2gb  5777  eliunxp  5807  dfres3  5968  restidsing  6039  ressn  6268  dflim2  6400  fncnv  6590  dff1o5  6812  respreima  7043  dff4  7078  dffo3  7079  dffo3f  7083  f1ompt  7088  fsn  7113  fconst3  7193  fconst4  7194  eufnfv  7209  dff13  7234  f1mpt  7241  isocnv3  7312  isores2  7313  isoini  7318  eloprabga  7501  mpomptx  7505  resoprab  7510  elrnmpores  7530  ov6g  7556  dfwe2  7753  dflim3  7823  dflim4  7824  dfopab2  8029  dfoprab3s  8030  dfoprab3  8031  fparlem1  8086  fparlem2  8087  fsplit  8091  brtpos2  8207  dftpos3  8219  tpostpos  8221  dfsmo2  8313  dfrecs3  8338  tz7.48-1  8409  ondif1  8465  ondif2  8466  elixp2  8879  xpcomco  9035  pssnn  9133  enfi  9151  eqinf  9428  infempty  9452  ttrclselem2  9678  frr2  9715  r0weon  9965  isinfcard  10045  dfac5lem1  10076  fpwwe  10601  axgroth6  10783  axgroth3  10786  elni2  10832  indpi  10862  recmulnq  10919  genpass  10964  lemul1a  12042  sup3  12146  elnn0z  12578  elznn0  12580  elznn  12581  eluz2b1  12917  eluz2b3  12920  elfz2nn0  13620  elfzo3  13679  shftidt2  15091  clim0  15516  fprod2dlem  15993  divalglem4  16413  ndvdsadd  16427  gcdaddmlem  16541  algfx  16597  isprm3  16700  isprm5  16725  isprm7  16726  xpsfrnel  17575  isacs2  17668  isfull2  17929  isfth2  17933  tosso  18432  odudlatb  18540  ismhm0  18807  issubmndb  18822  nsgacs  19186  isgim2  19288  isabl2  19813  iscyg3  19909  iscrng2  20281  isrnghmmul  20470  isrim  20520  isnzr2  20547  0ringdif  20556  isdomn6  20743  isdomn3  20744  isdrng2  20772  drngprop  20773  issdrg2  20824  islmim2  21113  islpir2  21380  iunocv  21713  ishil2  21751  islinds2  21845  ssntr  23098  isclo2  23128  isperf2  23192  isperf3  23193  nrmsep3  23395  isconn2  23454  iskgen3  23589  ptpjpre1  23611  tx1cn  23649  tx2cn  23650  hausdiag  23685  qustgplem  24161  istdrg2  24218  isngp2  24637  isngp3  24638  isnvc2  24739  isclmp  25139  iscvs  25169  isncvsngp  25191  ovoliunlem1  25544  ismbl2  25569  i1f1lem  25731  i1fres  25747  itg1climres  25756  pilem1  26491  ellogrn  26601  ellogdm  26681  1cubr  26884  atandm  26918  atandm2  26919  atandm3  26920  atandm4  26921  atans2  26973  eldmgm  27063  madeval2  27903  elnns2  28411  elzs2  28469  elznns  28472  elreno2  28565  isfusgrcl  29468  nbgrel  29487  iscusgrvtx  29568  iscusgredg  29570  dfpth2  29875  clwlkclwwlkflem  30152  isph  30971  h2hcau  31128  h2hlm  31129  issh2  31358  isch2  31372  h1dei  31699  elbdop2  32020  dfadj2  32034  cnvadj  32041  hhcno  32053  hhcnf  32054  eleigvec2  32107  riesz2  32215  rnbra  32256  elat2  32489  ofpreima  32817  mpomptxf  32830  f1od2  32871  maprnin  32883  xrofsup  32919  xrdifh  32932  sgn3da  32986  prmidl0  33598  cmpcref  34108  ofcfval  34356  ispisys2  34411  1stmbfm  34518  2ndmbfm  34519  eulerpartlems  34618  eulerpartlemgc  34620  eulerpartlemv  34622  eulerpartlemd  34624  eulerpartlemr  34632  eulerpartlemn  34639  ballotlemodife  34756  oddprm2  34913  bnj945  35033  bnj1172  35260  bnj1296  35280  snmlval  35645  rexxfr3dALT  35953  eldm3  36075  brtxp2  36193  brpprod3a  36198  dffun10  36226  elfuns  36227  brimg  36249  dfrdg4  36265  ellines  36466  opnrebl  36644  mh-regprimbi  36869  bj-ax12ig  37057  bj-equsexval  37096  bj-substw  37164  bj-csbsnlem  37352  bj-clel3gALT  37497  bj-mpomptALT  37573  bj-elid6  37626  bj-eldiag  37632  bj-imdiridlem  37641  bj-imdirco  37646  bj-isrvec  37750  taupilem3  37775  topdifinffinlem  37805  relowlssretop  37821  wl-dfclab  38052  istotbnd3  38234  isbnd2  38246  isbnd3b  38248  exidcl  38339  isdrngo2  38421  isdrngo3  38422  iscrngo2  38460  isdmn2  38518  isfldidl2  38532  isdmn3  38537  brres2  38736  eldmqsres  38756  brxrn2  38847  blockadjliftmap  38921  qmapeldisjsim  39323  petlem  39378  eldisjs7  39404  petseq  39439  islshpat  39605  iscvlat2N  39912  ishlat3N  39942  snatpsubN  40338  diclspsn  41782  redvmptabs  42933  reelznn0nn  43047  prjspeclsp  43158  isnacs2  43251  islnm2  43619  islnr2  43655  islnr3  43656  dflim7  43814  omge2  43839  minregex  44074  iscard5  44076  en2pr  44087  pren2  44093  elinintab  44115  elmapintab  44136  elinlem  44138  cnvcnvintabd  44140  sqrtcvallem1  44171  reabsifpos  44174  k0004lem1  44687  2reu8  47670  dfdfat2  47686  prproropf1olem0  48072  prprelb  48086  prprspr2  48088  isodd2  48221  iseven5  48250  isodd7  48251  oddprmne2  48301  clnbgrel  48414  sclnbgrelself  48434  dfvopnbgr2  48439  sgrp2sgrp  48814  eliunxp2  48920  mpomptx2  48921  elbigo  49137  tposres0  49462  opndisj  49488  isnrm4  49516  iscnrm3  49537  iscnrm4  49539  catprs  49596  initopropd  49828  termopropd  49829  zeroopropd  49830  catcsect  49983  2arwcatlem1  50180  setc1onsubc  50187