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  624  anabs5  664  abai  827  annotanannot  835  pm5.33  836  cases  1043  equsexALT  2424  2sb5rf  2477  2eu8  2660  eq2tri  2799  rexbiia  3083  rmobiia  3349  reubiia  3350  rabbiia  3394  ceqsrexbv  3599  euxfrw  3668  euxfr  3670  2reu5  3705  dfpss3  4030  eldifpr  4603  eldiftp  4632  eldifsn  4730  elrint  4932  elriin  5024  rabxp  5672  copsex2gb  5755  eliunxp  5786  dfres3  5943  restidsing  6012  ressn  6243  dflim2  6375  fncnv  6565  dff1o5  6783  respreima  7012  dff4  7047  dffo3  7048  dffo3f  7052  f1ompt  7057  fsn  7082  fconst3  7161  fconst4  7162  eufnfv  7177  dff13  7202  f1mpt  7209  isocnv3  7280  isores2  7281  isoini  7286  eloprabga  7469  mpomptx  7473  resoprab  7478  elrnmpores  7498  ov6g  7524  dfwe2  7721  dflim3  7791  dflim4  7792  dfopab2  7998  dfoprab3s  7999  dfoprab3  8000  fparlem1  8055  fparlem2  8056  fsplit  8060  brtpos2  8175  dftpos3  8187  tpostpos  8189  dfsmo2  8280  dfrecs3  8305  tz7.48-1  8375  ondif1  8429  ondif2  8430  elixp2  8842  xpcomco  8998  pssnn  9096  enfi  9114  eqinf  9391  infempty  9415  ttrclselem2  9638  frr2  9675  r0weon  9925  isinfcard  10005  dfac5lem1  10036  fpwwe  10560  axgroth6  10742  axgroth3  10745  elni2  10791  indpi  10821  recmulnq  10878  genpass  10923  lemul1a  12000  sup3  12104  elnn0z  12528  elznn0  12530  elznn  12531  eluz2b1  12860  eluz2b3  12863  elfz2nn0  13563  elfzo3  13622  shftidt2  15034  clim0  15459  fprod2dlem  15936  divalglem4  16356  ndvdsadd  16370  gcdaddmlem  16484  algfx  16540  isprm3  16643  isprm5  16668  isprm7  16669  xpsfrnel  17517  isacs2  17610  isfull2  17871  isfth2  17875  tosso  18374  odudlatb  18482  ismhm0  18749  issubmndb  18764  nsgacs  19128  isgim2  19231  isabl2  19756  iscyg3  19852  iscrng2  20224  isrnghmmul  20413  isrim  20462  isnzr2  20486  0ringdif  20495  isdomn6  20682  isdomn3  20683  isdrng2  20711  drngprop  20712  issdrg2  20763  islmim2  21053  islpir2  21320  iunocv  21671  ishil2  21709  islinds2  21803  ssntr  23033  isclo2  23063  isperf2  23127  isperf3  23128  nrmsep3  23330  isconn2  23389  iskgen3  23524  ptpjpre1  23546  tx1cn  23584  tx2cn  23585  hausdiag  23620  qustgplem  24096  istdrg2  24153  isngp2  24572  isngp3  24573  isnvc2  24674  isclmp  25074  iscvs  25104  isncvsngp  25126  ovoliunlem1  25479  ismbl2  25504  i1f1lem  25666  i1fres  25682  itg1climres  25691  pilem1  26429  ellogrn  26536  ellogdm  26616  1cubr  26819  atandm  26853  atandm2  26854  atandm3  26855  atandm4  26856  atans2  26908  eldmgm  26999  madeval2  27839  elnns2  28347  elzs2  28405  elznns  28408  elreno2  28501  isfusgrcl  29404  nbgrel  29423  iscusgrvtx  29504  iscusgredg  29506  dfpth2  29812  clwlkclwwlkflem  30089  isph  30908  h2hcau  31065  h2hlm  31066  issh2  31295  isch2  31309  h1dei  31636  elbdop2  31957  dfadj2  31971  cnvadj  31978  hhcno  31990  hhcnf  31991  eleigvec2  32044  riesz2  32152  rnbra  32193  elat2  32426  ofpreima  32753  mpomptxf  32766  f1od2  32807  maprnin  32819  xrofsup  32855  xrdifh  32868  sgn3da  32922  prmidl0  33525  cmpcref  34010  ofcfval  34258  ispisys2  34313  1stmbfm  34420  2ndmbfm  34421  eulerpartlems  34520  eulerpartlemgc  34522  eulerpartlemv  34524  eulerpartlemd  34526  eulerpartlemr  34534  eulerpartlemn  34541  ballotlemodife  34658  oddprm2  34815  bnj945  34932  bnj1172  35159  bnj1296  35179  snmlval  35529  rexxfr3dALT  35837  eldm3  35959  brtxp2  36077  brpprod3a  36082  dffun10  36110  elfuns  36111  brimg  36133  dfrdg4  36149  ellines  36350  opnrebl  36518  mh-regprimbi  36743  bj-ax12ig  36931  bj-equsexval  36970  bj-substw  37038  bj-csbsnlem  37226  bj-clel3gALT  37371  bj-mpomptALT  37447  bj-elid6  37500  bj-eldiag  37506  bj-imdiridlem  37515  bj-imdirco  37520  bj-isrvec  37624  taupilem3  37649  topdifinffinlem  37677  relowlssretop  37693  wl-dfclab  37924  istotbnd3  38106  isbnd2  38118  isbnd3b  38120  exidcl  38211  isdrngo2  38293  isdrngo3  38294  iscrngo2  38332  isdmn2  38390  isfldidl2  38404  isdmn3  38409  brres2  38608  eldmqsres  38628  brxrn2  38719  blockadjliftmap  38793  qmapeldisjsim  39195  petlem  39250  eldisjs7  39276  petseq  39311  islshpat  39477  iscvlat2N  39784  ishlat3N  39814  snatpsubN  40210  diclspsn  41654  redvmptabs  42806  reelznn0nn  42920  prjspeclsp  43059  isnacs2  43152  islnm2  43524  islnr2  43560  islnr3  43561  dflim7  43719  omge2  43744  minregex  43979  iscard5  43981  en2pr  43992  pren2  43998  elinintab  44020  elmapintab  44041  elinlem  44043  cnvcnvintabd  44045  sqrtcvallem1  44076  reabsifpos  44079  k0004lem1  44592  2reu8  47572  dfdfat2  47588  prproropf1olem0  47974  prprelb  47988  prprspr2  47990  isodd2  48123  iseven5  48152  isodd7  48153  oddprmne2  48203  clnbgrel  48316  sclnbgrelself  48336  dfvopnbgr2  48341  sgrp2sgrp  48716  eliunxp2  48822  mpomptx2  48823  elbigo  49039  tposres0  49364  opndisj  49390  isnrm4  49418  iscnrm3  49439  iscnrm4  49441  catprs  49498  initopropd  49730  termopropd  49731  zeroopropd  49732  catcsect  49885  2arwcatlem1  50082  setc1onsubc  50089