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  2451  2sb5rf  2504  2eu8  2686  eq2tri  2825  rexbiia  3111  rmobiia  3375  reubiia  3376  rabbiia  3420  ceqsrexbv  3613  euxfrw  3682  euxfr  3684  2reu5  3719  dfpss3  4019  eldifpr  4619  eldiftp  4648  eldifsn  4748  elrint  4952  elriin  5044  rabxp  5703  copsex2gb  5789  eliunxp  5820  dfres3  5986  restidsing  6057  ressn  6306  dflim2  6439  fncnv  6635  dff1o5  6856  respreima  7089  dff4  7125  dffo3  7126  dffo3f  7130  f1ompt  7135  fsn  7160  fconst3  7242  fconst4  7243  eufnfv  7258  dff13  7281  f1mpt  7288  isocnv3  7363  isores2  7364  isoini  7369  eloprabga  7552  mpomptx  7556  resoprab  7561  elrnmpores  7582  ov6g  7608  mpt3mpt  7709  dfwe2  7812  dflim3  7882  dflim4  7883  dfopab2  8088  dfoprab3s  8089  dfoprab3  8090  f1od2  8135  fparlem1  8150  fparlem2  8151  fsplit  8155  brtpos2  8277  dftpos3  8289  tpostpos  8291  dfsmo2  8383  dfrecs3  8408  tz7.48-1  8481  ondif1  8537  ondif2  8538  elixp2  8957  xpcomco  9114  pssnn  9212  enfi  9230  eqinf  9504  infempty  9528  ttrclselem2  9754  frr2  9791  r0weon  10118  isinfcard  10198  dfac5lem1  10229  fpwwe  10758  axgroth6  10940  axgroth3  10943  elni2  10989  indpi  11019  recmulnq  11076  genpass  11121  lemul1a  12198  sup3  12301  elnn0z  12733  elznn0  12735  elznn  12736  eluz2b1  13073  eluz2b3  13076  elfz2nn0  13779  elfzo3  13838  shftidt2  15263  sgn3da  15283  clim0  15702  fprod2dlem  16176  divalglem4  16595  ndvdsadd  16609  gcdaddmlem  16725  algfx  16784  isprm3  16887  isprm5  16912  isprm7  16913  xpsfrnel  17763  isacs2  17856  isfull2  18117  isfth2  18121  tosso  18620  odudlatb  18728  ismhm0  19014  issubmndb  19029  nsgacs  19401  isgim2  19508  isabl2  20034  iscyg3  20130  iscrng2  20509  isrnghmmul  20702  isrim  20758  isnzr2  20798  0ringdif  20808  isdomn6  20995  isdomn3  20996  drngprop  21028  isdrng3  21037  isdrng5  21038  issdrg2  21082  islmim2  21371  isfieldidl  21570  isfieldidl2  21571  prmidl0  21664  islpir2  21684  iunocv  22017  ishil2  22055  islinds2  22149  ssntr  23406  isclo2  23436  isperf2  23500  isperf3  23501  nrmsep3  23703  isconn2  23762  iskgen3  23898  ptpjpre1  23920  tx1cn  23958  tx2cn  23959  hausdiag  23994  qustgplem  24470  istdrg2  24527  isngp2  24946  isngp3  24947  isnvc2  25048  isclmp  25448  iscvs  25478  isncvsngp  25500  ovoliunlem1  25853  ismbl2  25878  i1f1lem  26040  i1fres  26056  itg1climres  26065  pilem1  26808  ellogrn  26917  ellogdm  26997  1cubr  27200  atandm  27234  atandm2  27235  atandm3  27236  atandm4  27237  atans2  27289  eldmgm  27379  madeval2  28249  elnns2  28757  elzs2  28815  elznns  28818  elreno2  28911  isfusgrcl  29932  nbgrel  29951  iscusgrvtx  30032  iscusgredg  30034  dfpth2  30344  clwlkclwwlkflem  30625  isph  31454  h2hcau  31611  h2hlm  31612  issh2  31841  isch2  31855  h1dei  32182  elbdop2  32503  dfadj2  32517  cnvadj  32524  hhcno  32536  hhcnf  32537  eleigvec2  32590  riesz2  32698  rnbra  32739  elat2  32972  ofpreima  33331  mpomptxf  33343  maprnin  33393  xrofsup  33429  xrdifh  33442  cmpcref  34552  ofcfval  34800  ispisys2  34856  1stmbfm  34962  2ndmbfm  34963  eulerpartlems  35062  eulerpartlemgc  35064  eulerpartlemv  35066  eulerpartlemd  35068  eulerpartlemr  35076  eulerpartlemn  35083  ballotlemodife  35200  oddprm2  35354  bnj945  35474  bnj1172  35701  bnj1296  35721  snmlval  36263  rexxfr3dALT  36571  eldm3  36704  brtxp2  36821  brpprod3a  36826  dffun10  36854  elfuns  36855  brimg  36877  dfrdg4  36893  ellines  37095  opnrebl  37286  mh-regprimbi  37511  bj-ax12ig  37698  bj-equsexval  37737  bj-substw  37805  bj-csbsnlem  37993  bj-clel3gALT  38154  bj-mpomptALT  38232  bj-elid6  38283  bj-eldiag  38289  bj-imdiridlem  38298  bj-imdirco  38303  bj-isrvec  38407  taupilem3  38432  topdifinffinlem  38462  relowlssretop  38478  wl-dfclab  38709  istotbnd3  38897  isbnd2  38909  isbnd3b  38911  exidcl  39002  isdrngo2  39084  isdrngo3  39085  iscrngo2  39123  isdmn2  39181  isfldidl2  39195  isdmn3  39200  brres2  39397  eldmqsres  39417  brxrn2  39508  blockadjliftmap  39582  qmapeldisjsim  39984  petlem  40039  eldisjs7  40065  petseq  40100  islshpat  40266  iscvlat2N  40573  ishlat3N  40603  snatpsubN  40999  diclspsn  42443  redvmptabs  43604  reelznn0nn  43718  prjspeclsp  43833  isnacs2  43910  islnm2  44273  islnr2  44308  islnr3  44309  dflim7  44467  omge2  44492  minregex  44727  iscard5  44729  en2pr  44740  pren2  44746  elinintab  44768  elmapintab  44788  elinlem  44790  cnvcnvintabd  44792  sqrtcvallem1  44823  reabsifpos  44826  k0004lem1  45339  2reu8  48388  dfdfat2  48403  prproropf1olem0  48789  prprelb  48803  prprspr2  48805  isodd2  48938  iseven5  48967  isodd7  48968  oddprmne2  49018  clnbgrel  49131  sclnbgrelself  49151  dfvopnbgr2  49156  sgrp2sgrp  49530  isidom3  49647  eliunxp2  49651  mpomptx2  49652  elbigo  49868  rrx2xpref1o  50036  tposres0  50195  opndisj  50222  isnrm4  50250  iscnrm3  50271  iscnrm4  50273  catprs  50330  initopropd  50570  termopropd  50571  zeroopropd  50572  catcsect  50738  2arwcatlem1  50938  setc1onsubc  50945  alsralrex  51188  alsraln0  51189  dfalseu2  51212