Theorem pm5.32i 585

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm5.32ri  586  anbi2i  635  anabs5  676  abai  839  annotanannot  848  pm5.33  849  cases  1058  equsexALT  2450  2sb5rf  2503  2eu8  2685  eq2tri  2824  rexbiia  3109  rmobiia  3373  reubiia  3374  rabbiia  3418  ceqsrexbv  3613  euxfrw  3682  euxfr  3684  2reu5  3719  dfpss3  4040  eldifpr  4622  eldiftp  4651  eldifsn  4751  elrint  4952  elriin  5045  rabxp  5707  copsex2gb  5791  eliunxp  5821  dfres3  5981  restidsing  6053  ressn  6287  dflim2  6420  fncnv  6610  dff1o5  6831  respreima  7062  dff4  7098  dffo3  7099  dffo3f  7103  f1ompt  7108  fsn  7133  fconst3  7216  fconst4  7217  eufnfv  7232  dff13  7255  f1mpt  7262  isocnv3  7337  isores2  7338  isoini  7343  eloprabga  7526  mpomptx  7530  resoprab  7535  elrnmpores  7555  ov6g  7581  dfwe2  7777  dflim3  7847  dflim4  7848  dfopab2  8053  dfoprab3s  8054  dfoprab3  8055  fparlem1  8113  fparlem2  8114  fsplit  8118  brtpos2  8234  dftpos3  8246  tpostpos  8248  dfsmo2  8340  dfrecs3  8365  tz7.48-1  8436  ondif1  8492  ondif2  8493  elixp2  8912  xpcomco  9069  pssnn  9167  enfi  9185  eqinf  9459  infempty  9483  ttrclselem2  9709  frr2  9746  r0weon  10019  isinfcard  10099  dfac5lem1  10130  fpwwe  10659  axgroth6  10841  axgroth3  10844  elni2  10890  indpi  10920  recmulnq  10977  genpass  11022  lemul1a  12097  sup3  12200  elnn0z  12632  elznn0  12634  elznn  12635  eluz2b1  12972  eluz2b3  12975  elfz2nn0  13677  elfzo3  13736  shftidt2  15158  sgn3da  15178  clim0  15597  fprod2dlem  16073  divalglem4  16492  ndvdsadd  16506  gcdaddmlem  16620  algfx  16676  isprm3  16779  isprm5  16804  isprm7  16805  xpsfrnel  17654  isacs2  17747  isfull2  18008  isfth2  18012  tosso  18511  odudlatb  18619  ismhm0  18904  issubmndb  18919  nsgacs  19291  isgim2  19398  isabl2  19923  iscyg3  20019  iscrng2  20397  isrnghmmul  20589  isrim  20645  isnzr2  20684  0ringdif  20694  isdomn6  20881  isdomn3  20882  isdrng2  20912  drngprop  20913  isdrng3  20922  isdrng5  20923  issdrg2  20967  islmim2  21256  isfieldidl  21455  isfieldidl2  21456  prmidl0  21547  islpir2  21567  iunocv  21900  ishil2  21938  islinds2  22032  ssntr  23289  isclo2  23319  isperf2  23383  isperf3  23384  nrmsep3  23586  isconn2  23645  iskgen3  23781  ptpjpre1  23803  tx1cn  23841  tx2cn  23842  hausdiag  23877  qustgplem  24353  istdrg2  24410  isngp2  24829  isngp3  24830  isnvc2  24931  isclmp  25331  iscvs  25361  isncvsngp  25383  ovoliunlem1  25736  ismbl2  25761  i1f1lem  25923  i1fres  25939  itg1climres  25948  pilem1  26694  ellogrn  26804  ellogdm  26884  1cubr  27087  atandm  27121  atandm2  27122  atandm3  27123  atandm4  27124  atans2  27176  eldmgm  27266  madeval2  28106  elnns2  28614  elzs2  28672  elznns  28675  elreno2  28768  isfusgrcl  29789  nbgrel  29808  iscusgrvtx  29889  iscusgredg  29891  dfpth2  30201  clwlkclwwlkflem  30482  isph  31311  h2hcau  31468  h2hlm  31469  issh2  31698  isch2  31712  h1dei  32039  elbdop2  32360  dfadj2  32374  cnvadj  32381  hhcno  32393  hhcnf  32394  eleigvec2  32447  riesz2  32555  rnbra  32596  elat2  32829  ofpreima  33146  mpomptxf  33159  f1od2  33198  maprnin  33210  xrofsup  33246  xrdifh  33259  cmpcref  34368  ofcfval  34616  ispisys2  34672  1stmbfm  34779  2ndmbfm  34780  eulerpartlems  34879  eulerpartlemgc  34881  eulerpartlemv  34883  eulerpartlemd  34885  eulerpartlemr  34893  eulerpartlemn  34900  ballotlemodife  35017  oddprm2  35171  bnj945  35291  bnj1172  35518  bnj1296  35538  snmlval  35918  rexxfr3dALT  36226  eldm3  36348  brtxp2  36466  brpprod3a  36471  dffun10  36499  elfuns  36500  brimg  36522  dfrdg4  36538  ellines  36740  opnrebl  36947  mh-regprimbi  37172  bj-ax12ig  37359  bj-equsexval  37398  bj-substw  37466  bj-csbsnlem  37654  bj-clel3gALT  37800  bj-mpomptALT  37877  bj-elid6  37930  bj-eldiag  37936  bj-imdiridlem  37945  bj-imdirco  37950  bj-isrvec  38054  taupilem3  38079  topdifinffinlem  38109  relowlssretop  38125  wl-dfclab  38356  istotbnd3  38529  isbnd2  38541  isbnd3b  38543  exidcl  38634  isdrngo2  38716  isdrngo3  38717  iscrngo2  38755  isdmn2  38813  isfldidl2  38827  isdmn3  38832  brres2  39029  eldmqsres  39049  brxrn2  39140  blockadjliftmap  39214  qmapeldisjsim  39616  petlem  39671  eldisjs7  39697  petseq  39732  islshpat  39898  iscvlat2N  40205  ishlat3N  40235  snatpsubN  40631  diclspsn  42075  redvmptabs  43243  reelznn0nn  43357  prjspeclsp  43466  isnacs2  43559  islnm2  43927  islnr2  43963  islnr3  43964  dflim7  44122  omge2  44147  minregex  44382  iscard5  44384  en2pr  44395  pren2  44401  elinintab  44423  elmapintab  44444  elinlem  44446  cnvcnvintabd  44448  sqrtcvallem1  44479  reabsifpos  44482  k0004lem1  44995  2reu8  48008  dfdfat2  48024  prproropf1olem0  48410  prprelb  48424  prprspr2  48426  isodd2  48559  iseven5  48588  isodd7  48589  oddprmne2  48639  clnbgrel  48752  sclnbgrelself  48772  dfvopnbgr2  48777  sgrp2sgrp  49151  isidom3  49268  eliunxp2  49272  mpomptx2  49273  elbigo  49489  tposres0  49811  opndisj  49837  isnrm4  49865  iscnrm3  49886  iscnrm4  49888  catprs  49945  initopropd  50177  termopropd  50178  zeroopropd  50179  catcsect  50332  2arwcatlem1  50529  setc1onsubc  50536  alsralrex  50749  alsraln0  50750  dfalseu2  50773