Theorem pm5.32i 573

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  pm5.32ri  574  anbi2i  621  anabs5  661  abai  825  annotanannot  833  pm5.33  834  cases  1040  equsexALT  2412  2sb5rf  2465  2eu8  2647  eq2tri  2792  rexbiia  3081  rmobiia  3369  reubiia  3370  rabbiia  3422  rabbiiaOLD  3423  ceqsrexbv  3639  euxfrw  3713  euxfr  3715  2reu5  3750  dfpss3  4082  eldifpr  4662  eldiftp  4692  eldifsn  4792  elrint  4995  elriin  5085  rabxp  5726  copsex2gb  5808  eliunxp  5840  dfres3  5990  restidsing  6057  ressn  6291  dflim2  6428  fncnv  6627  dff1o5  6847  respreima  7074  dff4  7110  dffo3  7111  dffo3f  7115  f1ompt  7120  fsn  7144  fconst3  7225  fconst4  7226  eufnfv  7241  dff13  7265  f1mpt  7271  isocnv3  7339  isores2  7340  isoini  7345  eloprabga  7528  eloprabgaOLD  7529  mpomptx  7533  resoprab  7538  elrnmpores  7559  ov6g  7585  dfwe2  7777  dflim3  7852  dflim4  7853  dfopab2  8057  dfoprab3s  8058  dfoprab3  8059  fparlem1  8117  fparlem2  8118  fsplit  8122  brtpos2  8238  dftpos3  8250  tpostpos  8252  dfsmo2  8368  dfrecs3  8393  dfrecs3OLD  8394  tz7.48-1  8464  ondif1  8522  ondif2  8523  elixp2  8920  xpcomco  9087  pssnn  9193  enfi  9215  eqinf  9509  infempty  9532  ttrclselem2  9751  frr2  9785  r0weon  10037  isinfcard  10117  dfac5lem1  10148  fpwwe  10671  axgroth6  10853  axgroth3  10856  elni2  10902  indpi  10932  recmulnq  10989  genpass  11034  lemul1a  12101  sup3  12204  elnn0z  12604  elznn0  12606  elznn  12607  eluz2b1  12936  eluz2b3  12939  elfz2nn0  13627  elfzo3  13684  shftidt2  15064  clim0  15486  fprod2dlem  15960  divalglem4  16376  ndvdsadd  16390  gcdaddmlem  16502  algfx  16554  isprm3  16657  isprm5  16681  isprm7  16682  xpsfrnel  17547  isacs2  17636  isfull2  17903  isfth2  17907  tosso  18414  odudlatb  18520  ismhm0  18750  issubmndb  18765  nsgacs  19125  isgim2  19228  isabl2  19757  iscyg3  19853  iscrng2  20204  isrnghmmul  20393  isrim  20443  isnzr2  20469  0ringdif  20476  isdrng2  20650  drngprop  20651  issdrg2  20695  islmim2  20963  islpir2  21237  isdomn3  21265  iunocv  21630  ishil2  21670  islinds2  21764  ssntr  23006  isclo2  23036  isperf2  23100  isperf3  23101  nrmsep3  23303  isconn2  23362  iskgen3  23497  ptpjpre1  23519  tx1cn  23557  tx2cn  23558  hausdiag  23593  qustgplem  24069  istdrg2  24126  isngp2  24550  isngp3  24551  isnvc2  24660  isclmp  25068  iscvs  25098  isncvsngp  25121  ovoliunlem1  25475  ismbl2  25500  i1f1lem  25662  i1fres  25679  itg1climres  25688  pilem1  26433  ellogrn  26538  ellogdm  26618  1cubr  26819  atandm  26853  atandm2  26854  atandm3  26855  atandm4  26856  atans2  26908  eldmgm  26999  madeval2  27826  elnns2  28261  isfusgrcl  29206  nbgrel  29225  iscusgrvtx  29306  iscusgredg  29308  clwlkclwwlkflem  29886  isph  30704  h2hcau  30861  h2hlm  30862  issh2  31091  isch2  31105  h1dei  31432  elbdop2  31753  dfadj2  31767  cnvadj  31774  hhcno  31786  hhcnf  31787  eleigvec2  31840  riesz2  31948  rnbra  31989  elat2  32222  ofpreima  32532  mpomptxf  32545  f1od2  32585  maprnin  32595  xrofsup  32619  xrdifh  32630  isdomn6  33071  prmidl0  33262  cmpcref  33582  ofcfval  33848  ispisys2  33903  1stmbfm  34011  2ndmbfm  34012  eulerpartlems  34111  eulerpartlemgc  34113  eulerpartlemv  34115  eulerpartlemd  34117  eulerpartlemr  34125  eulerpartlemn  34132  ballotlemodife  34248  sgn3da  34292  oddprm2  34418  bnj945  34535  bnj1172  34763  bnj1296  34783  snmlval  35072  eldm3  35486  brtxp2  35608  brpprod3a  35613  dffun10  35641  elfuns  35642  brimg  35664  dfrdg4  35678  ellines  35879  opnrebl  35935  bj-ax12ig  36243  bj-equsexval  36267  bj-substw  36330  bj-csbsnlem  36512  bj-clel3gALT  36658  bj-mpomptALT  36729  bj-elid6  36780  bj-eldiag  36786  bj-imdiridlem  36795  bj-imdirco  36800  bj-isrvec  36904  taupilem3  36929  topdifinffinlem  36957  relowlssretop  36973  wl-dfclab  37194  istotbnd3  37375  isbnd2  37387  isbnd3b  37389  exidcl  37480  isdrngo2  37562  isdrngo3  37563  iscrngo2  37601  isdmn2  37659  isfldidl2  37673  isdmn3  37678  brres2  37870  eldmqsres  37889  brxrn2  37977  petlem  38414  islshpat  38619  iscvlat2N  38926  ishlat3N  38956  snatpsubN  39353  diclspsn  40797  reelznn0nn  42139  prjspeclsp  42171  isnacs2  42268  islnm2  42644  islnr2  42680  islnr3  42681  dflim7  42844  omge2  42869  minregex  43106  iscard5  43108  en2pr  43119  pren2  43125  elinintab  43147  elmapintab  43168  elinlem  43170  cnvcnvintabd  43172  sqrtcvallem1  43203  reabsifpos  43206  k0004lem1  43719  2reu8  46630  dfdfat2  46646  prproropf1olem0  46979  prprelb  46993  prprspr2  46995  isodd2  47112  iseven5  47141  isodd7  47142  oddprmne2  47192  clnbgrel  47304  sclnbgrelself  47320  dfvopnbgr2  47325  sgrp2sgrp  47476  eliunxp2  47583  mpomptx2  47584  elbigo  47810  opndisj  48107  isnrm4  48135  iscnrm3  48157  iscnrm4  48159  catprs  48203