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  2417  2sb5rf  2470  2eu8  2652  eq2tri  2791  rexbiia  3074  rmobiia  3351  reubiia  3352  rabbiia  3400  rabbiiaOLD  3401  ceqsrexbv  3613  euxfrw  3683  euxfr  3685  2reu5  3720  dfpss3  4042  eldifpr  4612  eldiftp  4641  eldifsn  4740  elrint  4942  elriin  5033  rabxp  5671  copsex2gb  5753  eliunxp  5784  dfres3  5939  restidsing  6008  ressn  6237  dflim2  6369  fncnv  6559  dff1o5  6777  respreima  7004  dff4  7039  dffo3  7040  dffo3f  7044  f1ompt  7049  fsn  7073  fconst3  7153  fconst4  7154  eufnfv  7169  dff13  7195  f1mpt  7202  isocnv3  7273  isores2  7274  isoini  7279  eloprabga  7462  mpomptx  7466  resoprab  7471  elrnmpores  7491  ov6g  7517  dfwe2  7714  dflim3  7787  dflim4  7788  dfopab2  7994  dfoprab3s  7995  dfoprab3  7996  fparlem1  8052  fparlem2  8053  fsplit  8057  brtpos2  8172  dftpos3  8184  tpostpos  8186  dfsmo2  8277  dfrecs3  8302  tz7.48-1  8372  ondif1  8426  ondif2  8427  elixp2  8835  xpcomco  8991  pssnn  9092  enfi  9111  eqinf  9394  infempty  9418  ttrclselem2  9641  frr2  9675  r0weon  9925  isinfcard  10005  dfac5lem1  10036  fpwwe  10559  axgroth6  10741  axgroth3  10744  elni2  10790  indpi  10820  recmulnq  10877  genpass  10922  lemul1a  11996  sup3  12100  elnn0z  12502  elznn0  12504  elznn  12505  eluz2b1  12838  eluz2b3  12841  elfz2nn0  13539  elfzo3  13597  shftidt2  15006  clim0  15431  fprod2dlem  15905  divalglem4  16325  ndvdsadd  16339  gcdaddmlem  16453  algfx  16509  isprm3  16612  isprm5  16636  isprm7  16637  xpsfrnel  17484  isacs2  17577  isfull2  17838  isfth2  17842  tosso  18341  odudlatb  18449  ismhm0  18682  issubmndb  18697  nsgacs  19059  isgim2  19162  isabl2  19687  iscyg3  19783  iscrng2  20155  isrnghmmul  20345  isrim  20395  isnzr2  20421  0ringdif  20430  isdomn6  20617  isdomn3  20618  isdrng2  20646  drngprop  20647  issdrg2  20698  islmim2  20988  islpir2  21255  iunocv  21606  ishil2  21644  islinds2  21738  ssntr  22961  isclo2  22991  isperf2  23055  isperf3  23056  nrmsep3  23258  isconn2  23317  iskgen3  23452  ptpjpre1  23474  tx1cn  23512  tx2cn  23513  hausdiag  23548  qustgplem  24024  istdrg2  24081  isngp2  24501  isngp3  24502  isnvc2  24603  isclmp  25013  iscvs  25043  isncvsngp  25065  ovoliunlem1  25419  ismbl2  25444  i1f1lem  25606  i1fres  25622  itg1climres  25631  pilem1  26377  ellogrn  26484  ellogdm  26564  1cubr  26768  atandm  26802  atandm2  26803  atandm3  26804  atandm4  26805  atans2  26857  eldmgm  26948  madeval2  27781  elnns2  28256  elzs2  28310  elznns  28313  isfusgrcl  29284  nbgrel  29303  iscusgrvtx  29384  iscusgredg  29386  dfpth2  29692  clwlkclwwlkflem  29966  isph  30784  h2hcau  30941  h2hlm  30942  issh2  31171  isch2  31185  h1dei  31512  elbdop2  31833  dfadj2  31847  cnvadj  31854  hhcno  31866  hhcnf  31867  eleigvec2  31920  riesz2  32028  rnbra  32069  elat2  32302  ofpreima  32622  mpomptxf  32634  f1od2  32677  maprnin  32687  xrofsup  32723  xrdifh  32736  sgn3da  32792  prmidl0  33397  cmpcref  33816  ofcfval  34064  ispisys2  34119  1stmbfm  34227  2ndmbfm  34228  eulerpartlems  34327  eulerpartlemgc  34329  eulerpartlemv  34331  eulerpartlemd  34333  eulerpartlemr  34341  eulerpartlemn  34348  ballotlemodife  34465  oddprm2  34622  bnj945  34739  bnj1172  34967  bnj1296  34987  snmlval  35303  rexxfr3dALT  35611  eldm3  35733  brtxp2  35854  brpprod3a  35859  dffun10  35887  elfuns  35888  brimg  35910  dfrdg4  35924  ellines  36125  opnrebl  36293  bj-ax12ig  36609  bj-equsexval  36633  bj-substw  36695  bj-csbsnlem  36876  bj-clel3gALT  37021  bj-mpomptALT  37092  bj-elid6  37143  bj-eldiag  37149  bj-imdiridlem  37158  bj-imdirco  37163  bj-isrvec  37267  taupilem3  37292  topdifinffinlem  37320  relowlssretop  37336  wl-dfclab  37569  istotbnd3  37750  isbnd2  37762  isbnd3b  37764  exidcl  37855  isdrngo2  37937  isdrngo3  37938  iscrngo2  37976  isdmn2  38034  isfldidl2  38048  isdmn3  38053  brres2  38242  eldmqsres  38260  brxrn2  38342  petlem  38789  islshpat  38995  iscvlat2N  39302  ishlat3N  39332  snatpsubN  39729  diclspsn  41173  redvmptabs  42333  reelznn0nn  42434  prjspeclsp  42585  isnacs2  42679  islnm2  43051  islnr2  43087  islnr3  43088  dflim7  43246  omge2  43271  minregex  43507  iscard5  43509  en2pr  43520  pren2  43526  elinintab  43548  elmapintab  43569  elinlem  43571  cnvcnvintabd  43573  sqrtcvallem1  43604  reabsifpos  43607  k0004lem1  44120  2reu8  47097  dfdfat2  47113  prproropf1olem0  47487  prprelb  47501  prprspr2  47503  isodd2  47620  iseven5  47649  isodd7  47650  oddprmne2  47700  clnbgrel  47813  sclnbgrelself  47833  dfvopnbgr2  47838  sgrp2sgrp  48213  eliunxp2  48319  mpomptx2  48320  elbigo  48537  tposres0  48862  opndisj  48888  isnrm4  48916  iscnrm3  48937  iscnrm4  48939  catprs  48997  initopropd  49229  termopropd  49230  zeroopropd  49231  catcsect  49384  2arwcatlem1  49581  setc1onsubc  49588