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  2419  2sb5rf  2472  2eu8  2654  eq2tri  2793  rexbiia  3077  rmobiia  3352  reubiia  3353  rabbiia  3399  ceqsrexbv  3611  euxfrw  3680  euxfr  3682  2reu5  3717  dfpss3  4039  eldifpr  4611  eldiftp  4640  eldifsn  4738  elrint  4939  elriin  5029  rabxp  5664  copsex2gb  5746  eliunxp  5777  dfres3  5933  restidsing  6002  ressn  6232  dflim2  6364  fncnv  6554  dff1o5  6772  respreima  6999  dff4  7034  dffo3  7035  dffo3f  7039  f1ompt  7044  fsn  7068  fconst3  7147  fconst4  7148  eufnfv  7163  dff13  7188  f1mpt  7195  isocnv3  7266  isores2  7267  isoini  7272  eloprabga  7455  mpomptx  7459  resoprab  7464  elrnmpores  7484  ov6g  7510  dfwe2  7707  dflim3  7777  dflim4  7778  dfopab2  7984  dfoprab3s  7985  dfoprab3  7986  fparlem1  8042  fparlem2  8043  fsplit  8047  brtpos2  8162  dftpos3  8174  tpostpos  8176  dfsmo2  8267  dfrecs3  8292  tz7.48-1  8362  ondif1  8416  ondif2  8417  elixp2  8825  xpcomco  8980  pssnn  9078  enfi  9096  eqinf  9369  infempty  9393  ttrclselem2  9616  frr2  9650  r0weon  9900  isinfcard  9980  dfac5lem1  10011  fpwwe  10534  axgroth6  10716  axgroth3  10719  elni2  10765  indpi  10795  recmulnq  10852  genpass  10897  lemul1a  11972  sup3  12076  elnn0z  12478  elznn0  12480  elznn  12481  eluz2b1  12814  eluz2b3  12817  elfz2nn0  13515  elfzo3  13573  shftidt2  14985  clim0  15410  fprod2dlem  15884  divalglem4  16304  ndvdsadd  16318  gcdaddmlem  16432  algfx  16488  isprm3  16591  isprm5  16615  isprm7  16616  xpsfrnel  17463  isacs2  17556  isfull2  17817  isfth2  17821  tosso  18320  odudlatb  18428  ismhm0  18695  issubmndb  18710  nsgacs  19072  isgim2  19175  isabl2  19700  iscyg3  19796  iscrng2  20168  isrnghmmul  20358  isrim  20407  isnzr2  20431  0ringdif  20440  isdomn6  20627  isdomn3  20628  isdrng2  20656  drngprop  20657  issdrg2  20708  islmim2  20998  islpir2  21265  iunocv  21616  ishil2  21654  islinds2  21748  ssntr  22971  isclo2  23001  isperf2  23065  isperf3  23066  nrmsep3  23268  isconn2  23327  iskgen3  23462  ptpjpre1  23484  tx1cn  23522  tx2cn  23523  hausdiag  23558  qustgplem  24034  istdrg2  24091  isngp2  24510  isngp3  24511  isnvc2  24612  isclmp  25022  iscvs  25052  isncvsngp  25074  ovoliunlem1  25428  ismbl2  25453  i1f1lem  25615  i1fres  25631  itg1climres  25640  pilem1  26386  ellogrn  26493  ellogdm  26573  1cubr  26777  atandm  26811  atandm2  26812  atandm3  26813  atandm4  26814  atans2  26866  eldmgm  26957  madeval2  27792  elnns2  28267  elzs2  28321  elznns  28324  isfusgrcl  29297  nbgrel  29316  iscusgrvtx  29397  iscusgredg  29399  dfpth2  29705  clwlkclwwlkflem  29979  isph  30797  h2hcau  30954  h2hlm  30955  issh2  31184  isch2  31198  h1dei  31525  elbdop2  31846  dfadj2  31860  cnvadj  31867  hhcno  31879  hhcnf  31880  eleigvec2  31933  riesz2  32041  rnbra  32082  elat2  32315  ofpreima  32642  mpomptxf  32654  f1od2  32697  maprnin  32709  xrofsup  32745  xrdifh  32758  sgn3da  32812  prmidl0  33410  cmpcref  33858  ofcfval  34106  ispisys2  34161  1stmbfm  34268  2ndmbfm  34269  eulerpartlems  34368  eulerpartlemgc  34370  eulerpartlemv  34372  eulerpartlemd  34374  eulerpartlemr  34382  eulerpartlemn  34389  ballotlemodife  34506  oddprm2  34663  bnj945  34780  bnj1172  35008  bnj1296  35028  snmlval  35363  rexxfr3dALT  35671  eldm3  35793  brtxp2  35914  brpprod3a  35919  dffun10  35947  elfuns  35948  brimg  35970  dfrdg4  35984  ellines  36185  opnrebl  36353  bj-ax12ig  36669  bj-equsexval  36693  bj-substw  36755  bj-csbsnlem  36936  bj-clel3gALT  37081  bj-mpomptALT  37152  bj-elid6  37203  bj-eldiag  37209  bj-imdiridlem  37218  bj-imdirco  37223  bj-isrvec  37327  taupilem3  37352  topdifinffinlem  37380  relowlssretop  37396  wl-dfclab  37629  istotbnd3  37810  isbnd2  37822  isbnd3b  37824  exidcl  37915  isdrngo2  37997  isdrngo3  37998  iscrngo2  38036  isdmn2  38094  isfldidl2  38108  isdmn3  38113  brres2  38302  eldmqsres  38320  brxrn2  38402  petlem  38849  islshpat  39055  iscvlat2N  39362  ishlat3N  39392  snatpsubN  39788  diclspsn  41232  redvmptabs  42392  reelznn0nn  42493  prjspeclsp  42644  isnacs2  42738  islnm2  43110  islnr2  43146  islnr3  43147  dflim7  43305  omge2  43330  minregex  43566  iscard5  43568  en2pr  43579  pren2  43585  elinintab  43607  elmapintab  43628  elinlem  43630  cnvcnvintabd  43632  sqrtcvallem1  43663  reabsifpos  43666  k0004lem1  44179  2reu8  47142  dfdfat2  47158  prproropf1olem0  47532  prprelb  47546  prprspr2  47548  isodd2  47665  iseven5  47694  isodd7  47695  oddprmne2  47745  clnbgrel  47858  sclnbgrelself  47878  dfvopnbgr2  47883  sgrp2sgrp  48258  eliunxp2  48364  mpomptx2  48365  elbigo  48582  tposres0  48907  opndisj  48933  isnrm4  48961  iscnrm3  48982  iscnrm4  48984  catprs  49042  initopropd  49274  termopropd  49275  zeroopropd  49276  catcsect  49429  2arwcatlem1  49626  setc1onsubc  49633