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  3360  reubiia  3361  rabbiia  3409  rabbiiaOLD  3410  ceqsrexbv  3622  euxfrw  3692  euxfr  3694  2reu5  3729  dfpss3  4052  eldifpr  4622  eldiftp  4651  eldifsn  4750  elrint  4953  elriin  5045  rabxp  5686  copsex2gb  5769  eliunxp  5801  dfres3  5955  restidsing  6024  ressn  6258  dflim2  6390  fncnv  6589  dff1o5  6809  respreima  7038  dff4  7073  dffo3  7074  dffo3f  7078  f1ompt  7083  fsn  7107  fconst3  7187  fconst4  7188  eufnfv  7203  dff13  7229  f1mpt  7236  isocnv3  7307  isores2  7308  isoini  7313  eloprabga  7498  mpomptx  7502  resoprab  7507  elrnmpores  7527  ov6g  7553  dfwe2  7750  dflim3  7823  dflim4  7824  dfopab2  8031  dfoprab3s  8032  dfoprab3  8033  fparlem1  8091  fparlem2  8092  fsplit  8096  brtpos2  8211  dftpos3  8223  tpostpos  8225  dfsmo2  8316  dfrecs3  8341  tz7.48-1  8411  ondif1  8465  ondif2  8466  elixp2  8874  xpcomco  9031  pssnn  9132  enfi  9151  eqinf  9436  infempty  9460  ttrclselem2  9679  frr2  9713  r0weon  9965  isinfcard  10045  dfac5lem1  10076  fpwwe  10599  axgroth6  10781  axgroth3  10784  elni2  10830  indpi  10860  recmulnq  10917  genpass  10962  lemul1a  12036  sup3  12140  elnn0z  12542  elznn0  12544  elznn  12545  eluz2b1  12878  eluz2b3  12881  elfz2nn0  13579  elfzo3  13637  shftidt2  15047  clim0  15472  fprod2dlem  15946  divalglem4  16366  ndvdsadd  16380  gcdaddmlem  16494  algfx  16550  isprm3  16653  isprm5  16677  isprm7  16678  xpsfrnel  17525  isacs2  17614  isfull2  17875  isfth2  17879  tosso  18378  odudlatb  18484  ismhm0  18717  issubmndb  18732  nsgacs  19094  isgim2  19197  isabl2  19720  iscyg3  19816  iscrng2  20161  isrnghmmul  20351  isrim  20401  isnzr2  20427  0ringdif  20436  isdomn6  20623  isdomn3  20624  isdrng2  20652  drngprop  20653  issdrg2  20704  islmim2  20973  islpir2  21240  iunocv  21590  ishil2  21628  islinds2  21722  ssntr  22945  isclo2  22975  isperf2  23039  isperf3  23040  nrmsep3  23242  isconn2  23301  iskgen3  23436  ptpjpre1  23458  tx1cn  23496  tx2cn  23497  hausdiag  23532  qustgplem  24008  istdrg2  24065  isngp2  24485  isngp3  24486  isnvc2  24587  isclmp  24997  iscvs  25027  isncvsngp  25049  ovoliunlem1  25403  ismbl2  25428  i1f1lem  25590  i1fres  25606  itg1climres  25615  pilem1  26361  ellogrn  26468  ellogdm  26548  1cubr  26752  atandm  26786  atandm2  26787  atandm3  26788  atandm4  26789  atans2  26841  eldmgm  26932  madeval2  27761  elnns2  28233  elzs2  28287  elznns  28290  isfusgrcl  29248  nbgrel  29267  iscusgrvtx  29348  iscusgredg  29350  dfpth2  29659  clwlkclwwlkflem  29933  isph  30751  h2hcau  30908  h2hlm  30909  issh2  31138  isch2  31152  h1dei  31479  elbdop2  31800  dfadj2  31814  cnvadj  31821  hhcno  31833  hhcnf  31834  eleigvec2  31887  riesz2  31995  rnbra  32036  elat2  32269  ofpreima  32589  mpomptxf  32601  f1od2  32644  maprnin  32654  xrofsup  32690  xrdifh  32703  sgn3da  32759  prmidl0  33421  cmpcref  33840  ofcfval  34088  ispisys2  34143  1stmbfm  34251  2ndmbfm  34252  eulerpartlems  34351  eulerpartlemgc  34353  eulerpartlemv  34355  eulerpartlemd  34357  eulerpartlemr  34365  eulerpartlemn  34372  ballotlemodife  34489  oddprm2  34646  bnj945  34763  bnj1172  34991  bnj1296  35011  snmlval  35318  rexxfr3dALT  35626  eldm3  35748  brtxp2  35869  brpprod3a  35874  dffun10  35902  elfuns  35903  brimg  35925  dfrdg4  35939  ellines  36140  opnrebl  36308  bj-ax12ig  36624  bj-equsexval  36648  bj-substw  36710  bj-csbsnlem  36891  bj-clel3gALT  37036  bj-mpomptALT  37107  bj-elid6  37158  bj-eldiag  37164  bj-imdiridlem  37173  bj-imdirco  37178  bj-isrvec  37282  taupilem3  37307  topdifinffinlem  37335  relowlssretop  37351  wl-dfclab  37584  istotbnd3  37765  isbnd2  37777  isbnd3b  37779  exidcl  37870  isdrngo2  37952  isdrngo3  37953  iscrngo2  37991  isdmn2  38049  isfldidl2  38063  isdmn3  38068  brres2  38257  eldmqsres  38275  brxrn2  38357  petlem  38804  islshpat  39010  iscvlat2N  39317  ishlat3N  39347  snatpsubN  39744  diclspsn  41188  redvmptabs  42348  reelznn0nn  42449  prjspeclsp  42600  isnacs2  42694  islnm2  43067  islnr2  43103  islnr3  43104  dflim7  43262  omge2  43287  minregex  43523  iscard5  43525  en2pr  43536  pren2  43542  elinintab  43564  elmapintab  43585  elinlem  43587  cnvcnvintabd  43589  sqrtcvallem1  43620  reabsifpos  43623  k0004lem1  44136  2reu8  47113  dfdfat2  47129  prproropf1olem0  47503  prprelb  47517  prprspr2  47519  isodd2  47636  iseven5  47665  isodd7  47666  oddprmne2  47716  clnbgrel  47829  sclnbgrelself  47848  dfvopnbgr2  47853  sgrp2sgrp  48216  eliunxp2  48322  mpomptx2  48323  elbigo  48540  tposres0  48865  opndisj  48891  isnrm4  48919  iscnrm3  48940  iscnrm4  48942  catprs  49000  initopropd  49232  termopropd  49233  zeroopropd  49234  catcsect  49387  2arwcatlem1  49584  setc1onsubc  49591