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  623  anabs5  663  abai  826  annotanannot  834  pm5.33  835  cases  1042  equsexALT  2422  2sb5rf  2475  2eu8  2657  eq2tri  2796  rexbiia  3080  rmobiia  3370  reubiia  3371  rabbiia  3424  rabbiiaOLD  3425  ceqsrexbv  3640  euxfrw  3711  euxfr  3713  2reu5  3748  dfpss3  4071  eldifpr  4640  eldiftp  4669  eldifsn  4768  elrint  4971  elriin  5063  rabxp  5715  copsex2gb  5798  eliunxp  5830  dfres3  5984  restidsing  6053  ressn  6287  dflim2  6422  fncnv  6620  dff1o5  6838  respreima  7067  dff4  7102  dffo3  7103  dffo3f  7107  f1ompt  7112  fsn  7136  fconst3  7216  fconst4  7217  eufnfv  7232  dff13  7258  f1mpt  7264  isocnv3  7335  isores2  7336  isoini  7341  eloprabga  7525  mpomptx  7529  resoprab  7534  elrnmpores  7554  ov6g  7580  dfwe2  7777  dflim3  7851  dflim4  7852  dfopab2  8060  dfoprab3s  8061  dfoprab3  8062  fparlem1  8120  fparlem2  8121  fsplit  8125  brtpos2  8240  dftpos3  8252  tpostpos  8254  dfsmo2  8370  dfrecs3  8395  dfrecs3OLD  8396  tz7.48-1  8466  ondif1  8522  ondif2  8523  elixp2  8924  xpcomco  9085  pssnn  9191  enfi  9210  eqinf  9507  infempty  9530  ttrclselem2  9749  frr2  9783  r0weon  10035  isinfcard  10115  dfac5lem1  10146  fpwwe  10669  axgroth6  10851  axgroth3  10854  elni2  10900  indpi  10930  recmulnq  10987  genpass  11032  lemul1a  12104  sup3  12208  elnn0z  12610  elznn0  12612  elznn  12613  eluz2b1  12944  eluz2b3  12947  elfz2nn0  13641  elfzo3  13699  shftidt2  15103  clim0  15525  fprod2dlem  15999  divalglem4  16416  ndvdsadd  16430  gcdaddmlem  16544  algfx  16600  isprm3  16703  isprm5  16727  isprm7  16728  xpsfrnel  17583  isacs2  17672  isfull2  17934  isfth2  17938  tosso  18438  odudlatb  18544  ismhm0  18777  issubmndb  18792  nsgacs  19154  isgim2  19257  isabl2  19781  iscyg3  19877  iscrng2  20222  isrnghmmul  20415  isrim  20465  isnzr2  20491  0ringdif  20500  isdomn6  20687  isdomn3  20688  isdrng2  20716  drngprop  20717  issdrg2  20769  islmim2  21038  islpir2  21307  iunocv  21666  ishil2  21706  islinds2  21800  ssntr  23031  isclo2  23061  isperf2  23125  isperf3  23126  nrmsep3  23328  isconn2  23387  iskgen3  23522  ptpjpre1  23544  tx1cn  23582  tx2cn  23583  hausdiag  23618  qustgplem  24094  istdrg2  24151  isngp2  24573  isngp3  24574  isnvc2  24675  isclmp  25085  iscvs  25115  isncvsngp  25138  ovoliunlem1  25492  ismbl2  25517  i1f1lem  25679  i1fres  25695  itg1climres  25704  pilem1  26450  ellogrn  26556  ellogdm  26636  1cubr  26840  atandm  26874  atandm2  26875  atandm3  26876  atandm4  26877  atans2  26929  eldmgm  27020  madeval2  27847  elnns2  28299  elzs2  28340  elznns  28343  isfusgrcl  29285  nbgrel  29304  iscusgrvtx  29385  iscusgredg  29387  dfpth2  29696  clwlkclwwlkflem  29970  isph  30788  h2hcau  30945  h2hlm  30946  issh2  31175  isch2  31189  h1dei  31516  elbdop2  31837  dfadj2  31851  cnvadj  31858  hhcno  31870  hhcnf  31871  eleigvec2  31924  riesz2  32032  rnbra  32073  elat2  32306  ofpreima  32622  mpomptxf  32634  f1od2  32679  maprnin  32689  xrofsup  32718  xrdifh  32729  prmidl0  33419  cmpcref  33790  ofcfval  34040  ispisys2  34095  1stmbfm  34203  2ndmbfm  34204  eulerpartlems  34303  eulerpartlemgc  34305  eulerpartlemv  34307  eulerpartlemd  34309  eulerpartlemr  34317  eulerpartlemn  34324  ballotlemodife  34441  sgn3da  34485  oddprm2  34611  bnj945  34728  bnj1172  34956  bnj1296  34976  snmlval  35277  rexxfr3dALT  35585  eldm3  35702  brtxp2  35823  brpprod3a  35828  dffun10  35856  elfuns  35857  brimg  35879  dfrdg4  35893  ellines  36094  opnrebl  36262  bj-ax12ig  36578  bj-equsexval  36602  bj-substw  36664  bj-csbsnlem  36845  bj-clel3gALT  36990  bj-mpomptALT  37061  bj-elid6  37112  bj-eldiag  37118  bj-imdiridlem  37127  bj-imdirco  37132  bj-isrvec  37236  taupilem3  37261  topdifinffinlem  37289  relowlssretop  37305  wl-dfclab  37538  istotbnd3  37719  isbnd2  37731  isbnd3b  37733  exidcl  37824  isdrngo2  37906  isdrngo3  37907  iscrngo2  37945  isdmn2  38003  isfldidl2  38017  isdmn3  38022  brres2  38210  eldmqsres  38229  brxrn2  38317  petlem  38754  islshpat  38959  iscvlat2N  39266  ishlat3N  39296  snatpsubN  39693  diclspsn  41137  redvmptabs  42335  reelznn0nn  42424  prjspeclsp  42567  isnacs2  42662  islnm2  43035  islnr2  43071  islnr3  43072  dflim7  43231  omge2  43256  minregex  43492  iscard5  43494  en2pr  43505  pren2  43511  elinintab  43533  elmapintab  43554  elinlem  43556  cnvcnvintabd  43558  sqrtcvallem1  43589  reabsifpos  43592  k0004lem1  44105  2reu8  47070  dfdfat2  47086  prproropf1olem0  47435  prprelb  47449  prprspr2  47451  isodd2  47568  iseven5  47597  isodd7  47598  oddprmne2  47648  clnbgrel  47761  sclnbgrelself  47780  dfvopnbgr2  47785  sgrp2sgrp  48090  eliunxp2  48196  mpomptx2  48197  elbigo  48418  tposres0  48724  opndisj  48748  isnrm4  48776  iscnrm3  48797  iscnrm4  48799  catprs  48856