Theorem pm5.32i 566

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  pm5.32ri  567  anbi2i  611  anabs5  645  biadan2  844  abai  848  annotanannot  854  pm5.33  855  cases  1056  equsexvw  2101  equsexv  2277  equsexALT  2460  2sb5rf  2611  2eu8  2724  eq2tri  2867  rexbiia  3228  reubiia  3316  rmobiia  3321  rabbiia  3374  ceqsrexbv  3531  euxfr  3590  2reu5  3614  dfpss3  3891  eldifpr  4398  eldiftp  4420  eldifsn  4508  elrint  4710  elriin  4785  reuxfrd  5090  opeqsnOLD  5158  rabxp  5354  copsex2gb  5431  eliunxp  5461  dfres3  5602  restidsing  5670  ressn  5885  dflim2  5993  fncnv  6169  dff1o5  6358  respreima  6562  dff4  6591  dffo3  6592  f1ompt  6599  fsn  6621  fconst3  6698  fconst4  6699  eufnfv  6712  dff13  6732  f1mpt  6738  isocnv3  6802  isores2  6803  isoini  6808  eloprabga  6973  mpt2mptx  6977  resoprab  6982  elrnmpt2res  7000  ov6g  7024  dfwe2  7207  dflim3  7273  dflim4  7274  dfopab2  7450  dfoprab3s  7451  dfoprab3  7452  fparlem1  7507  fparlem2  7508  brtpos2  7589  dftpos3  7601  tpostpos  7603  dfsmo2  7676  dfrecs3  7701  tz7.48-1  7770  ondif1  7814  ondif2  7815  elixp2  8145  xpcomco  8285  eqinf  8625  infempty  8647  r0weon  9114  isinfcard  9194  dfac5lem1  9225  fpwwe  9749  axgroth6  9931  axgroth3  9934  elni2  9980  indpi  10010  recmulnq  10067  genpass  10112  lemul1a  11158  sup3  11261  elnn0z  11652  elznn0  11654  elznn  11655  eluz2b1  11974  eluz2b3  11977  elfz2nn0  12650  elfzo3  12706  shftidt2  14040  clim0  14456  fprod2dlem  14927  divalglem4  15335  ndvdsadd  15349  gcdaddmlem  15460  algfx  15508  isprm3  15610  isprm5  15632  isprm7  15633  xpsfrnel  16424  isacs2  16514  isfull2  16771  isfth2  16775  tosso  17237  odudlatb  17397  nsgacs  17828  isgim2  17905  isabl2  18398  iscyg3  18485  iscrng2  18761  isdrng2  18957  drngprop  18958  islmim2  19269  islpir2  19456  isnzr2  19468  iunocv  20232  ishil2  20270  islinds2  20359  ssntr  21073  isclo2  21103  isperf2  21167  isperf3  21168  nrmsep3  21370  isconn2  21428  iskgen3  21563  ptpjpre1  21585  tx1cn  21623  tx2cn  21624  hausdiag  21659  qustgplem  22134  istdrg2  22191  isngp2  22611  isngp3  22612  isnvc2  22713  isclmp  23106  iscvs  23136  isncvsngp  23158  ovoliunlem1  23482  ismbl2  23507  i1f1lem  23669  i1fres  23685  itg1climres  23694  pilem1  24418  ellogrn  24519  ellogdm  24598  1cubr  24782  atandm  24816  atandm2  24817  atandm3  24818  atandm4  24819  atans2  24871  eldmgm  24961  isfusgrcl  26428  nbgrel  26448  iscusgrvtx  26544  iscusgredg  26546  clwlkclwwlkflem  27146  isph  28004  h2hcau  28163  h2hlm  28164  issh2  28393  isch2  28407  h1dei  28736  elbdop2  29057  dfadj2  29071  cnvadj  29078  hhcno  29090  hhcnf  29091  eleigvec2  29144  riesz2  29252  rnbra  29293  elat2  29526  ofpreima  29791  mpt2mptxf  29803  f1od2  29825  maprnin  29832  xrofsup  29859  xrdifh  29868  cmpcref  30241  ofcfval  30484  ispisys2  30540  1stmbfm  30646  2ndmbfm  30647  eulerpartlems  30746  eulerpartlemgc  30748  eulerpartlemv  30750  eulerpartlemd  30752  eulerpartlemr  30760  eulerpartlemn  30767  ballotlemodife  30883  sgn3da  30927  oddprm2  31057  bnj945  31165  bnj1172  31390  bnj1296  31410  snmlval  31634  eldm3  31971  madeval2  32255  brtxp2  32307  brpprod3a  32312  dffun10  32340  elfuns  32341  brimg  32363  dfrdg4  32377  ellines  32578  opnrebl  32634  bj-ax12ig  32928  bj-equsexval  32951  bj-cleljustab  33157  bj-csbsnlem  33204  bj-mpt2mptALT  33381  bj-elid3  33401  bj-eldiag  33406  taupilem3  33480  topdifinffinlem  33509  relowlssretop  33525  istotbnd3  33879  isbnd2  33891  isbnd3b  33893  exidcl  33984  isdrngo2  34066  isdrngo3  34067  iscrngo2  34105  isdmn2  34163  isfldidl2  34177  isdmn3  34182  brres2  34350  eldmqsres  34366  brxrn2  34448  islshpat  34795  iscvlat2N  35102  ishlat3N  35132  snatpsubN  35528  diclspsn  36972  isnacs2  37768  islnm2  38146  islnr2  38182  islnr3  38183  issdrg2  38266  isdomn3  38280  elinintab  38378  elmapintab  38399  elinlem  38401  cnvcnvintabd  38403  k0004lem1  38942  dffo3f  39850  2reu8  41701  dfdfat2  41714  isodd2  42120  iseven5  42148  isodd7  42149  oddprmne2  42196  ismhm0  42370  sgrp2sgrp  42429  0ringdif  42435  isrnghmmul  42458  eliunxp2  42677  mpt2mptx2  42678  elbigo  42910