Theorem pm5.32i 577

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

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

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 399

This theorem is referenced by:  pm5.32ri  578  anbi2i  624  anabs5  661  abai  824  annotanannot  832  pm5.33  833  cases  1037  equsexvwOLD  2012  equsexv  2269  equsexALT  2441  2sb5rf  2496  2eu8  2744  eq2tri  2883  rexbiia  3246  reubiia  3390  rmobiia  3395  rabbiia  3472  ceqsrexbv  3650  euxfrw  3712  euxfr  3714  2reu5  3749  dfpss3  4063  eldifpr  4597  eldiftp  4624  eldifsn  4719  elrint  4917  elriin  5003  rabxp  5600  copsex2gb  5679  eliunxp  5708  dfres3  5858  restidsing  5922  ressn  6136  dflim2  6247  fncnv  6427  dff1o5  6624  respreima  6836  dff4  6867  dffo3  6868  f1ompt  6875  fsn  6897  fconst3  6976  fconst4  6977  eufnfv  6991  dff13  7013  f1mpt  7019  isocnv3  7085  isores2  7086  isoini  7091  eloprabga  7261  mpomptx  7265  resoprab  7270  elrnmpores  7288  ov6g  7312  dfwe2  7496  dflim3  7562  dflim4  7563  dfopab2  7750  dfoprab3s  7751  dfoprab3  7752  fparlem1  7807  fparlem2  7808  fsplit  7812  brtpos2  7898  dftpos3  7910  tpostpos  7912  dfsmo2  7984  dfrecs3  8009  tz7.48-1  8079  ondif1  8126  ondif2  8127  elixp2  8465  xpcomco  8607  eqinf  8948  infempty  8971  r0weon  9438  isinfcard  9518  dfac5lem1  9549  fpwwe  10068  axgroth6  10250  axgroth3  10253  elni2  10299  indpi  10329  recmulnq  10386  genpass  10431  lemul1a  11494  sup3  11598  elnn0z  11995  elznn0  11997  elznn  11998  eluz2b1  12320  eluz2b3  12323  elfz2nn0  12999  elfzo3  13055  shftidt2  14440  clim0  14863  fprod2dlem  15334  divalglem4  15747  ndvdsadd  15761  gcdaddmlem  15872  algfx  15924  isprm3  16027  isprm5  16051  isprm7  16052  xpsfrnel  16835  isacs2  16924  isfull2  17181  isfth2  17185  tosso  17646  odudlatb  17806  issubmndb  17970  nsgacs  18314  isgim2  18405  isabl2  18915  iscyg3  19005  iscrng2  19313  isdrng2  19512  drngprop  19513  issdrg2  19577  islmim2  19838  islpir2  20024  isnzr2  20036  iunocv  20825  ishil2  20863  islinds2  20957  ssntr  21666  isclo2  21696  isperf2  21760  isperf3  21761  nrmsep3  21963  isconn2  22022  iskgen3  22157  ptpjpre1  22179  tx1cn  22217  tx2cn  22218  hausdiag  22253  qustgplem  22729  istdrg2  22786  isngp2  23206  isngp3  23207  isnvc2  23308  isclmp  23701  iscvs  23731  isncvsngp  23753  ovoliunlem1  24103  ismbl2  24128  i1f1lem  24290  i1fres  24306  itg1climres  24315  pilem1  25039  ellogrn  25143  ellogdm  25222  1cubr  25420  atandm  25454  atandm2  25455  atandm3  25456  atandm4  25457  atans2  25509  eldmgm  25599  isfusgrcl  27103  nbgrel  27122  iscusgrvtx  27203  iscusgredg  27205  clwlkclwwlkflem  27782  isph  28599  h2hcau  28756  h2hlm  28757  issh2  28986  isch2  29000  h1dei  29327  elbdop2  29648  dfadj2  29662  cnvadj  29669  hhcno  29681  hhcnf  29682  eleigvec2  29735  riesz2  29843  rnbra  29884  elat2  30117  ofpreima  30410  mpomptxf  30425  f1od2  30457  maprnin  30467  xrofsup  30492  xrdifh  30503  cmpcref  31114  ofcfval  31357  ispisys2  31412  1stmbfm  31518  2ndmbfm  31519  eulerpartlems  31618  eulerpartlemgc  31620  eulerpartlemv  31622  eulerpartlemd  31624  eulerpartlemr  31632  eulerpartlemn  31639  ballotlemodife  31755  sgn3da  31799  oddprm2  31926  bnj945  32045  bnj1172  32273  bnj1296  32293  snmlval  32578  eldm3  32997  frr2  33145  madeval2  33290  brtxp2  33342  brpprod3a  33347  dffun10  33375  elfuns  33376  brimg  33398  dfrdg4  33412  ellines  33613  opnrebl  33668  bj-ax12ig  33969  bj-equsexval  33993  bj-csbsnlem  34223  bj-mpomptALT  34414  bj-elid6  34465  bj-eldiag  34471  bj-imdirid  34478  taupilem3  34603  topdifinffinlem  34631  relowlssretop  34647  wl-dfclab  34843  istotbnd3  35064  isbnd2  35076  isbnd3b  35078  exidcl  35169  isdrngo2  35251  isdrngo3  35252  iscrngo2  35290  isdmn2  35348  isfldidl2  35362  isdmn3  35367  brres2  35544  eldmqsres  35558  brxrn2  35642  islshpat  36168  iscvlat2N  36475  ishlat3N  36505  snatpsubN  36901  diclspsn  38345  prjspeclsp  39311  isnacs2  39352  islnm2  39727  islnr2  39763  islnr3  39764  isdomn3  39853  iscard5  39950  en2pr  39955  pren2  39961  elinintab  39984  elmapintab  40005  elinlem  40007  cnvcnvintabd  40009  k0004lem1  40546  dffo3f  41487  2reu8  43360  dfdfat2  43376  prproropf1olem0  43713  prprelb  43727  prprspr2  43729  isodd2  43849  iseven5  43878  isodd7  43879  oddprmne2  43929  ismhm0  44121  sgrp2sgrp  44184  0ringdif  44190  isrnghmmul  44213  eliunxp2  44431  mpomptx2  44432  elbigo  44660