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 229	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  pm5.32ri  575  anbi2i  622  anabs5  659  abai  823  annotanannot  831  pm5.33  832  cases  1039  equsexALT  2420  2sb5rf  2473  2eu8  2661  eq2tri  2806  rexbiia  3178  reubiia  3322  rmobiia  3328  rabbiia  3404  ceqsrexbv  3587  euxfrw  3659  euxfr  3661  2reu5  3696  dfpss3  4025  eldifpr  4598  eldiftp  4627  eldifsn  4725  elrint  4927  elriin  5014  rabxp  5634  copsex2gb  5713  eliunxp  5743  dfres3  5893  restidsing  5959  ressn  6185  dflim2  6319  fncnv  6503  dff1o5  6721  respreima  6937  dff4  6971  dffo3  6972  f1ompt  6979  fsn  7001  fconst3  7083  fconst4  7084  eufnfv  7099  dff13  7122  f1mpt  7128  isocnv3  7196  isores2  7197  isoini  7202  eloprabga  7373  eloprabgaOLD  7374  mpomptx  7378  resoprab  7383  elrnmpores  7402  ov6g  7427  dfwe2  7615  dflim3  7682  dflim4  7683  dfopab2  7878  dfoprab3s  7879  dfoprab3  7880  fparlem1  7936  fparlem2  7937  fsplit  7941  brtpos2  8032  dftpos3  8044  tpostpos  8046  dfsmo2  8162  dfrecs3  8187  dfrecs3OLD  8188  tz7.48-1  8258  ondif1  8307  ondif2  8308  elixp2  8663  xpcomco  8818  pssnn  8916  enfi  8938  eqinf  9204  infempty  9227  ttrclselem2  9445  frr2  9502  r0weon  9752  isinfcard  9832  dfac5lem1  9863  fpwwe  10386  axgroth6  10568  axgroth3  10571  elni2  10617  indpi  10647  recmulnq  10704  genpass  10749  lemul1a  11812  sup3  11915  elnn0z  12315  elznn0  12317  elznn  12318  eluz2b1  12641  eluz2b3  12644  elfz2nn0  13329  elfzo3  13385  shftidt2  14773  clim0  15196  fprod2dlem  15671  divalglem4  16086  ndvdsadd  16100  gcdaddmlem  16212  algfx  16266  isprm3  16369  isprm5  16393  isprm7  16394  xpsfrnel  17254  isacs2  17343  isfull2  17608  isfth2  17612  tosso  18118  odudlatb  18224  issubmndb  18425  nsgacs  18771  isgim2  18862  isabl2  19376  iscyg3  19467  iscrng2  19783  isdrng2  19982  drngprop  19983  issdrg2  20047  islmim2  20309  islpir2  20503  isnzr2  20515  iunocv  20867  ishil2  20907  islinds2  21001  ssntr  22190  isclo2  22220  isperf2  22284  isperf3  22285  nrmsep3  22487  isconn2  22546  iskgen3  22681  ptpjpre1  22703  tx1cn  22741  tx2cn  22742  hausdiag  22777  qustgplem  23253  istdrg2  23310  isngp2  23734  isngp3  23735  isnvc2  23844  isclmp  24241  iscvs  24271  isncvsngp  24294  ovoliunlem1  24647  ismbl2  24672  i1f1lem  24834  i1fres  24851  itg1climres  24860  pilem1  25591  ellogrn  25696  ellogdm  25775  1cubr  25973  atandm  26007  atandm2  26008  atandm3  26009  atandm4  26010  atans2  26062  eldmgm  26152  isfusgrcl  27669  nbgrel  27688  iscusgrvtx  27769  iscusgredg  27771  clwlkclwwlkflem  28347  isph  29163  h2hcau  29320  h2hlm  29321  issh2  29550  isch2  29564  h1dei  29891  elbdop2  30212  dfadj2  30226  cnvadj  30233  hhcno  30245  hhcnf  30246  eleigvec2  30299  riesz2  30407  rnbra  30448  elat2  30681  ofpreima  30981  mpomptxf  30995  f1od2  31035  maprnin  31045  xrofsup  31069  xrdifh  31080  prmidl0  31605  cmpcref  31779  ofcfval  32045  ispisys2  32100  1stmbfm  32206  2ndmbfm  32207  eulerpartlems  32306  eulerpartlemgc  32308  eulerpartlemv  32310  eulerpartlemd  32312  eulerpartlemr  32320  eulerpartlemn  32327  ballotlemodife  32443  sgn3da  32487  oddprm2  32614  bnj945  32732  bnj1172  32960  bnj1296  32980  snmlval  33272  eldm3  33707  madeval2  34016  brtxp2  34162  brpprod3a  34167  dffun10  34195  elfuns  34196  brimg  34218  dfrdg4  34232  ellines  34433  opnrebl  34488  bj-ax12ig  34796  bj-equsexval  34820  bj-substw  34883  bj-csbsnlem  35067  bj-clel3gALT  35200  bj-mpomptALT  35269  bj-elid6  35320  bj-eldiag  35326  bj-imdiridlem  35335  bj-imdirco  35340  bj-isrvec  35444  taupilem3  35469  topdifinffinlem  35497  relowlssretop  35513  wl-dfclab  35726  istotbnd3  35908  isbnd2  35920  isbnd3b  35922  exidcl  36013  isdrngo2  36095  isdrngo3  36096  iscrngo2  36134  isdmn2  36192  isfldidl2  36206  isdmn3  36211  brres2  36386  eldmqsres  36400  brxrn2  36484  islshpat  37010  iscvlat2N  37317  ishlat3N  37347  snatpsubN  37743  diclspsn  39187  prjspeclsp  40431  isnacs2  40508  islnm2  40883  islnr2  40919  islnr3  40920  isdomn3  41009  iscard5  41103  en2pr  41107  pren2  41113  elinintab  41136  elmapintab  41157  elinlem  41159  cnvcnvintabd  41161  sqrtcvallem1  41192  reabsifneg  41193  reabsifpos  41195  k0004lem1  41710  dffo3f  42670  2reu8  44555  dfdfat2  44571  prproropf1olem0  44906  prprelb  44920  prprspr2  44922  isodd2  45039  iseven5  45068  isodd7  45069  oddprmne2  45119  ismhm0  45311  sgrp2sgrp  45374  0ringdif  45380  isrnghmmul  45403  eliunxp2  45621  mpomptx2  45622  elbigo  45849  opndisj  46148  isnrm4  46176  iscnrm3  46198  iscnrm4  46200  catprs  46244