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  2449  2sb5rf  2502  2eu8  2684  eq2tri  2823  rexbiia  3108  rmobiia  3372  reubiia  3373  rabbiia  3417  ceqsrexbv  3610  euxfrw  3679  euxfr  3681  2reu5  3716  dfpss3  4037  eldifpr  4619  eldiftp  4648  eldifsn  4748  elrint  4949  elriin  5041  rabxp  5699  copsex2gb  5784  eliunxp  5814  dfres3  5975  restidsing  6047  ressn  6281  dflim2  6414  fncnv  6605  dff1o5  6826  respreima  7057  dff4  7093  dffo3  7094  dffo3f  7098  f1ompt  7103  fsn  7128  fconst3  7211  fconst4  7212  eufnfv  7227  dff13  7250  f1mpt  7257  isocnv3  7332  isores2  7333  isoini  7338  eloprabga  7521  mpomptx  7525  resoprab  7530  elrnmpores  7550  ov6g  7576  mpt3mpt  7677  dfwe2  7777  dflim3  7847  dflim4  7848  dfopab2  8052  dfoprab3s  8053  dfoprab3  8054  fparlem1  8112  fparlem2  8113  fsplit  8117  brtpos2  8233  dftpos3  8245  tpostpos  8247  dfsmo2  8339  dfrecs3  8364  tz7.48-1  8437  ondif1  8493  ondif2  8494  elixp2  8913  xpcomco  9070  pssnn  9168  enfi  9186  eqinf  9461  infempty  9485  ttrclselem2  9711  frr2  9748  r0weon  10072  isinfcard  10152  dfac5lem1  10183  fpwwe  10712  axgroth6  10894  axgroth3  10897  elni2  10943  indpi  10973  recmulnq  11030  genpass  11075  lemul1a  12152  sup3  12255  elnn0z  12687  elznn0  12689  elznn  12690  eluz2b1  13027  eluz2b3  13030  elfz2nn0  13732  elfzo3  13791  shftidt2  15214  sgn3da  15234  clim0  15653  fprod2dlem  16127  divalglem4  16546  ndvdsadd  16560  gcdaddmlem  16676  algfx  16735  isprm3  16838  isprm5  16863  isprm7  16864  xpsfrnel  17714  isacs2  17807  isfull2  18068  isfth2  18072  tosso  18571  odudlatb  18679  ismhm0  18965  issubmndb  18980  nsgacs  19352  isgim2  19459  isabl2  19984  iscyg3  20080  iscrng2  20459  isrnghmmul  20652  isrim  20708  isnzr2  20748  0ringdif  20758  isdomn6  20945  isdomn3  20946  drngprop  20978  isdrng3  20987  isdrng5  20988  issdrg2  21032  islmim2  21321  isfieldidl  21520  isfieldidl2  21521  prmidl0  21614  islpir2  21634  iunocv  21967  ishil2  22005  islinds2  22099  ssntr  23356  isclo2  23386  isperf2  23450  isperf3  23451  nrmsep3  23653  isconn2  23712  iskgen3  23848  ptpjpre1  23870  tx1cn  23908  tx2cn  23909  hausdiag  23944  qustgplem  24420  istdrg2  24477  isngp2  24896  isngp3  24897  isnvc2  24998  isclmp  25398  iscvs  25428  isncvsngp  25450  ovoliunlem1  25803  ismbl2  25828  i1f1lem  25990  i1fres  26006  itg1climres  26015  pilem1  26760  ellogrn  26869  ellogdm  26949  1cubr  27152  atandm  27186  atandm2  27187  atandm3  27188  atandm4  27189  atans2  27241  eldmgm  27331  madeval2  28201  elnns2  28709  elzs2  28767  elznns  28770  elreno2  28863  isfusgrcl  29884  nbgrel  29903  iscusgrvtx  29984  iscusgredg  29986  dfpth2  30296  clwlkclwwlkflem  30577  isph  31406  h2hcau  31563  h2hlm  31564  issh2  31793  isch2  31807  h1dei  32134  elbdop2  32455  dfadj2  32469  cnvadj  32476  hhcno  32488  hhcnf  32489  eleigvec2  32542  riesz2  32650  rnbra  32691  elat2  32924  ofpreima  33241  mpomptxf  33254  f1od2  33293  maprnin  33305  xrofsup  33341  xrdifh  33354  cmpcref  34464  ofcfval  34712  ispisys2  34768  1stmbfm  34875  2ndmbfm  34876  eulerpartlems  34975  eulerpartlemgc  34977  eulerpartlemv  34979  eulerpartlemd  34981  eulerpartlemr  34989  eulerpartlemn  34996  ballotlemodife  35113  oddprm2  35267  bnj945  35387  bnj1172  35614  bnj1296  35634  snmlval  36065  rexxfr3dALT  36373  eldm3  36495  brtxp2  36613  brpprod3a  36618  dffun10  36646  elfuns  36647  brimg  36669  dfrdg4  36685  ellines  36887  opnrebl  37078  mh-regprimbi  37303  bj-ax12ig  37490  bj-equsexval  37529  bj-substw  37597  bj-csbsnlem  37785  bj-clel3gALT  37931  bj-mpomptALT  38008  bj-elid6  38059  bj-eldiag  38065  bj-imdiridlem  38074  bj-imdirco  38079  bj-isrvec  38183  taupilem3  38208  topdifinffinlem  38238  relowlssretop  38254  wl-dfclab  38485  istotbnd3  38673  isbnd2  38685  isbnd3b  38687  exidcl  38778  isdrngo2  38860  isdrngo3  38861  iscrngo2  38899  isdmn2  38957  isfldidl2  38971  isdmn3  38976  brres2  39173  eldmqsres  39193  brxrn2  39284  blockadjliftmap  39358  qmapeldisjsim  39760  petlem  39815  eldisjs7  39841  petseq  39876  islshpat  40042  iscvlat2N  40349  ishlat3N  40379  snatpsubN  40775  diclspsn  42219  redvmptabs  43379  reelznn0nn  43493  prjspeclsp  43602  isnacs2  43670  islnm2  44038  islnr2  44074  islnr3  44075  dflim7  44233  omge2  44258  minregex  44493  iscard5  44495  en2pr  44506  pren2  44512  elinintab  44534  elmapintab  44555  elinlem  44557  cnvcnvintabd  44559  sqrtcvallem1  44590  reabsifpos  44593  k0004lem1  45106  2reu8  48126  dfdfat2  48142  prproropf1olem0  48528  prprelb  48542  prprspr2  48544  isodd2  48677  iseven5  48706  isodd7  48707  oddprmne2  48757  clnbgrel  48870  sclnbgrelself  48890  dfvopnbgr2  48895  sgrp2sgrp  49269  isidom3  49386  eliunxp2  49390  mpomptx2  49391  elbigo  49607  tposres0  49929  opndisj  49955  isnrm4  49983  iscnrm3  50004  iscnrm4  50006  catprs  50063  initopropd  50295  termopropd  50296  zeroopropd  50297  catcsect  50450  2arwcatlem1  50647  setc1onsubc  50654  alsralrex  50852  alsraln0  50853  dfalseu2  50876