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  2423  2sb5rf  2476  2eu8  2659  eq2tri  2798  rexbiia  3082  rmobiia  3348  reubiia  3349  rabbiia  3393  ceqsrexbv  3598  euxfrw  3667  euxfr  3669  2reu5  3704  dfpss3  4029  eldifpr  4602  eldiftp  4631  eldifsn  4731  elrint  4931  elriin  5023  rabxp  5679  copsex2gb  5762  eliunxp  5792  dfres3  5949  restidsing  6018  ressn  6249  dflim2  6381  fncnv  6571  dff1o5  6789  respreima  7018  dff4  7053  dffo3  7054  dffo3f  7058  f1ompt  7063  fsn  7088  fconst3  7168  fconst4  7169  eufnfv  7184  dff13  7209  f1mpt  7216  isocnv3  7287  isores2  7288  isoini  7293  eloprabga  7476  mpomptx  7480  resoprab  7485  elrnmpores  7505  ov6g  7531  dfwe2  7728  dflim3  7798  dflim4  7799  dfopab2  8005  dfoprab3s  8006  dfoprab3  8007  fparlem1  8062  fparlem2  8063  fsplit  8067  brtpos2  8182  dftpos3  8194  tpostpos  8196  dfsmo2  8287  dfrecs3  8312  tz7.48-1  8382  ondif1  8436  ondif2  8437  elixp2  8849  xpcomco  9005  pssnn  9103  enfi  9121  eqinf  9398  infempty  9422  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  12009  sup3  12113  elnn0z  12537  elznn0  12539  elznn  12540  eluz2b1  12869  eluz2b3  12872  elfz2nn0  13572  elfzo3  13631  shftidt2  15043  clim0  15468  fprod2dlem  15945  divalglem4  16365  ndvdsadd  16379  gcdaddmlem  16493  algfx  16549  isprm3  16652  isprm5  16677  isprm7  16678  xpsfrnel  17526  isacs2  17619  isfull2  17880  isfth2  17884  tosso  18383  odudlatb  18491  ismhm0  18758  issubmndb  18773  nsgacs  19137  isgim2  19240  isabl2  19765  iscyg3  19861  iscrng2  20233  isrnghmmul  20422  isrim  20471  isnzr2  20495  0ringdif  20504  isdomn6  20691  isdomn3  20692  isdrng2  20720  drngprop  20721  issdrg2  20772  islmim2  21061  islpir2  21328  iunocv  21661  ishil2  21699  islinds2  21793  ssntr  23023  isclo2  23053  isperf2  23117  isperf3  23118  nrmsep3  23320  isconn2  23379  iskgen3  23514  ptpjpre1  23536  tx1cn  23574  tx2cn  23575  hausdiag  23610  qustgplem  24086  istdrg2  24143  isngp2  24562  isngp3  24563  isnvc2  24664  isclmp  25064  iscvs  25094  isncvsngp  25116  ovoliunlem1  25469  ismbl2  25494  i1f1lem  25656  i1fres  25672  itg1climres  25681  pilem1  26416  ellogrn  26523  ellogdm  26603  1cubr  26806  atandm  26840  atandm2  26841  atandm3  26842  atandm4  26843  atans2  26895  eldmgm  26985  madeval2  27825  elnns2  28333  elzs2  28391  elznns  28394  elreno2  28487  isfusgrcl  29390  nbgrel  29409  iscusgrvtx  29490  iscusgredg  29492  dfpth2  29797  clwlkclwwlkflem  30074  isph  30893  h2hcau  31050  h2hlm  31051  issh2  31280  isch2  31294  h1dei  31621  elbdop2  31942  dfadj2  31956  cnvadj  31963  hhcno  31975  hhcnf  31976  eleigvec2  32029  riesz2  32137  rnbra  32178  elat2  32411  ofpreima  32738  mpomptxf  32751  f1od2  32792  maprnin  32804  xrofsup  32840  xrdifh  32853  sgn3da  32907  prmidl0  33510  cmpcref  33994  ofcfval  34242  ispisys2  34297  1stmbfm  34404  2ndmbfm  34405  eulerpartlems  34504  eulerpartlemgc  34506  eulerpartlemv  34508  eulerpartlemd  34510  eulerpartlemr  34518  eulerpartlemn  34525  ballotlemodife  34642  oddprm2  34799  bnj945  34916  bnj1172  35143  bnj1296  35163  snmlval  35513  rexxfr3dALT  35821  eldm3  35943  brtxp2  36061  brpprod3a  36066  dffun10  36094  elfuns  36095  brimg  36117  dfrdg4  36133  ellines  36334  opnrebl  36502  mh-regprimbi  36727  bj-ax12ig  36915  bj-equsexval  36954  bj-substw  37022  bj-csbsnlem  37210  bj-clel3gALT  37355  bj-mpomptALT  37431  bj-elid6  37484  bj-eldiag  37490  bj-imdiridlem  37499  bj-imdirco  37504  bj-isrvec  37608  taupilem3  37633  topdifinffinlem  37663  relowlssretop  37679  wl-dfclab  37910  istotbnd3  38092  isbnd2  38104  isbnd3b  38106  exidcl  38197  isdrngo2  38279  isdrngo3  38280  iscrngo2  38318  isdmn2  38376  isfldidl2  38390  isdmn3  38395  brres2  38594  eldmqsres  38614  brxrn2  38705  blockadjliftmap  38779  qmapeldisjsim  39181  petlem  39236  eldisjs7  39262  petseq  39297  islshpat  39463  iscvlat2N  39770  ishlat3N  39800  snatpsubN  40196  diclspsn  41640  redvmptabs  42792  reelznn0nn  42906  prjspeclsp  43045  isnacs2  43138  islnm2  43506  islnr2  43542  islnr3  43543  dflim7  43701  omge2  43726  minregex  43961  iscard5  43963  en2pr  43974  pren2  43980  elinintab  44002  elmapintab  44023  elinlem  44025  cnvcnvintabd  44027  sqrtcvallem1  44058  reabsifpos  44061  k0004lem1  44574  2reu8  47560  dfdfat2  47576  prproropf1olem0  47962  prprelb  47976  prprspr2  47978  isodd2  48111  iseven5  48140  isodd7  48141  oddprmne2  48191  clnbgrel  48304  sclnbgrelself  48324  dfvopnbgr2  48329  sgrp2sgrp  48704  eliunxp2  48810  mpomptx2  48811  elbigo  49027  tposres0  49352  opndisj  49378  isnrm4  49406  iscnrm3  49427  iscnrm4  49429  catprs  49486  initopropd  49718  termopropd  49719  zeroopropd  49720  catcsect  49873  2arwcatlem1  50070  setc1onsubc  50077