Theorem pm5.32i 570

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  pm5.32ri  571  anbi2i  616  anabs5  653  biadan2OLD  814  abai  818  annotanannot  825  pm5.33  826  cases  1026  equsexvw  2051  equsexv  2241  equsexALT  2383  2sb5rf  2529  2eu8  2688  eq2tri  2840  rexbiia  3222  reubiia  3314  rmobiia  3319  rabbiia  3380  ceqsrexbv  3539  euxfr  3603  2reu5  3632  dfpss3  3914  eldifpr  4425  eldiftp  4454  eldifsn  4549  elrint  4751  elriin  4826  reuxfrd  5132  opeqsnOLD  5200  rabxp  5400  copsex2gb  5477  eliunxp  5505  dfres3  5647  restidsing  5714  ressn  5925  dflim2  6032  fncnv  6207  dff1o5  6400  respreima  6608  dff4  6637  dffo3  6638  f1ompt  6645  fsn  6667  fconst3  6749  fconst4  6750  eufnfv  6763  dff13  6784  f1mpt  6790  isocnv3  6854  isores2  6855  isoini  6860  eloprabga  7024  mpt2mptx  7028  resoprab  7033  elrnmpt2res  7051  ov6g  7075  dfwe2  7259  dflim3  7325  dflim4  7326  dfopab2  7501  dfoprab3s  7502  dfoprab3  7503  fparlem1  7558  fparlem2  7559  brtpos2  7640  dftpos3  7652  tpostpos  7654  dfsmo2  7727  dfrecs3  7752  tz7.48-1  7821  ondif1  7865  ondif2  7866  elixp2  8198  xpcomco  8338  eqinf  8678  infempty  8701  r0weon  9168  isinfcard  9248  dfac5lem1  9279  fpwwe  9803  axgroth6  9985  axgroth3  9988  elni2  10034  indpi  10064  recmulnq  10121  genpass  10166  lemul1a  11231  sup3  11334  elnn0z  11741  elznn0  11743  elznn  11744  eluz2b1  12066  eluz2b3  12069  elfz2nn0  12749  elfzo3  12805  shftidt2  14228  clim0  14645  fprod2dlem  15113  divalglem4  15526  ndvdsadd  15540  gcdaddmlem  15651  algfx  15699  isprm3  15801  isprm5  15823  isprm7  15824  xpsfrnel  16609  isacs2  16699  isfull2  16956  isfth2  16960  tosso  17422  odudlatb  17582  nsgacs  18014  isgim2  18091  isabl2  18587  iscyg3  18674  iscrng2  18950  isdrng2  19149  drngprop  19150  islmim2  19461  islpir2  19648  isnzr2  19660  iunocv  20424  ishil2  20462  islinds2  20556  ssntr  21270  isclo2  21300  isperf2  21364  isperf3  21365  nrmsep3  21567  isconn2  21626  iskgen3  21761  ptpjpre1  21783  tx1cn  21821  tx2cn  21822  hausdiag  21857  qustgplem  22332  istdrg2  22389  isngp2  22809  isngp3  22810  isnvc2  22911  isclmp  23304  iscvs  23334  isncvsngp  23356  ovoliunlem1  23706  ismbl2  23731  i1f1lem  23893  i1fres  23909  itg1climres  23918  pilem1  24642  ellogrn  24743  ellogdm  24822  1cubr  25020  atandm  25054  atandm2  25055  atandm3  25056  atandm4  25057  atans2  25109  eldmgm  25200  isfusgrcl  26668  nbgrel  26687  iscusgrvtx  26769  iscusgredg  26771  clwlkclwwlkflem  27386  isph  28249  h2hcau  28408  h2hlm  28409  issh2  28638  isch2  28652  h1dei  28981  elbdop2  29302  dfadj2  29316  cnvadj  29323  hhcno  29335  hhcnf  29336  eleigvec2  29389  riesz2  29497  rnbra  29538  elat2  29771  ofpreima  30030  mpt2mptxf  30043  f1od2  30065  maprnin  30072  xrofsup  30098  xrdifh  30106  cmpcref  30515  ofcfval  30758  ispisys2  30814  1stmbfm  30920  2ndmbfm  30921  eulerpartlems  31020  eulerpartlemgc  31022  eulerpartlemv  31024  eulerpartlemd  31026  eulerpartlemr  31034  eulerpartlemn  31041  ballotlemodife  31158  sgn3da  31202  oddprm2  31335  bnj945  31443  bnj1172  31668  bnj1296  31688  snmlval  31912  eldm3  32245  madeval2  32525  brtxp2  32577  brpprod3a  32582  dffun10  32610  elfuns  32611  brimg  32633  dfrdg4  32647  ellines  32848  opnrebl  32903  bj-ax12ig  33194  bj-equsexval  33228  bj-cleljustab  33422  bj-csbsnlem  33469  bj-mpt2mptALT  33645  bj-elid3  33665  bj-eldiag  33670  taupilem3  33761  topdifinffinlem  33790  relowlssretop  33806  istotbnd3  34178  isbnd2  34190  isbnd3b  34192  exidcl  34283  isdrngo2  34365  isdrngo3  34366  iscrngo2  34404  isdmn2  34462  isfldidl2  34476  isdmn3  34481  brres2  34651  eldmqsres  34667  brxrn2  34749  islshpat  35155  iscvlat2N  35462  ishlat3N  35492  snatpsubN  35888  diclspsn  37332  isnacs2  38211  islnm2  38589  islnr2  38625  islnr3  38626  issdrg2  38709  isdomn3  38723  elinintab  38820  elmapintab  38841  elinlem  38843  cnvcnvintabd  38845  k0004lem1  39383  dffo3f  40269  2reu8  42135  dfdfat2  42151  prproropf1olem0  42423  prprelb  42437  prprspr2  42439  isodd2  42555  iseven5  42583  isodd7  42584  oddprmne2  42631  ismhm0  42802  sgrp2sgrp  42861  0ringdif  42867  isrnghmmul  42890  eliunxp2  43109  mpt2mptx2  43110  elbigo  43342