Theorem pm4.71rd 562

Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)

Hypothesis

Ref	Expression
pm4.71rd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
pm4.71rd	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Proof of Theorem pm4.71rd

Step	Hyp	Ref	Expression
1		pm4.71rd.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	pm4.71d 561	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	2	biancomd 463	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:  reueubd  3407  2reu5  3780  ralss  4083  rexss  4084  eqrrabd  4109  rabsneq  4666  reuhypd  5437  exopxfr2  5869  dfco2a  6277  onunel  6500  feu  6797  fcnvres  6798  funbrfv2b  6979  dffn5  6980  feqmptdf  6992  fimarab  6996  eqfnfv2  7065  dff4  7135  fmptco  7163  dff13  7292  opiota  8100  mpoxopovel  8261  brtpos  8276  dftpos3  8285  erinxp  8849  qliftfun  8860  pw2f1olem  9142  infm3  12254  prime  12724  predfz  13710  hashf1lem2  14505  hashle2prv  14527  oddnn02np1  16396  oddge22np1  16397  evennn02n  16398  evennn2n  16399  smueqlem  16536  vdwmc2  17026  acsfiel  17712  subsubc  17917  ismgmid  18703  eqger  19218  eqgid  19220  ghmqusker  19327  gaorber  19348  symgfix2  19458  znleval  21596  psrbaglefi  21969  bastop2  23022  elcls2  23103  maxlp  23176  restopn2  23206  restdis  23207  1stccn  23492  tx1cn  23638  tx2cn  23639  imasnopn  23719  imasncld  23720  imasncls  23721  idqtop  23735  tgqtop  23741  filuni  23914  uffix2  23953  cnflf  24031  isfcls  24038  fclsopn  24043  cnfcf  24071  ptcmplem2  24082  xmeter  24464  imasf1oxms  24523  prdsbl  24525  caucfil  25336  cfilucfil4  25374  shft2rab  25562  sca2rab  25566  mbfinf  25719  i1f1lem  25743  i1fres  25760  itg1climres  25769  mbfi1fseqlem4  25773  iblpos  25848  itgposval  25851  cnplimc  25942  ply1remlem  26224  plyremlem  26364  dvdsflsumcom  27249  fsumvma2  27276  vmasum  27278  logfac2  27279  chpchtsum  27281  logfaclbnd  27284  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  dchrisum0lem1  27578  colinearalg  28943  nbusgreledg  29388  nbusgredgeu0  29403  umgr2v2enb1  29562  iswwlksnx  29873  wspniunwspnon  29956  clwlknf1oclwwlknlem2  30114  clwlknf1oclwwlkn  30116  eupth2lem2  30251  eupth2lems  30270  frgrncvvdeqlem2  30332  fusgr2wsp2nb  30366  fusgreg2wsp  30368  pjpreeq  31430  elnlfn  31960  nfpconfp  32651  fmptcof2  32675  dfcnv2  32694  2ndpreima  32719  f1od2  32735  fpwrelmap  32747  iocinioc2  32784  nndiffz1  32791  algextdeglem6  33713  indpi1  33984  1stmbfm  34225  2ndmbfm  34226  eulerpartlemgh  34343  bnj1171  34976  mrsubrn  35481  elfuns  35879  fneval  36318  bj-imdirval3  37150  topdifinfindis  37312  uncf  37559  phpreu  37564  poimirlem23  37603  poimirlem26  37606  poimirlem27  37607  areacirclem5  37672  erimeq2  38634  prter3  38838  islshpat  38973  lfl1dim  39077  glbconxN  39335  cdlemefrs29bpre0  40353  dib1dim  41122  dib1dim2  41125  diclspsn  41151  dihopelvalcpre  41205  dih1dimatlem  41286  mapdordlem1a  41591  hdmapoc  41888  prjspeclsp  42567  rmydioph  42971  pw2f1ocnv  42994  onsupeqnmax  43208  orddif0suc  43230  cantnf2  43287  tfsconcat0i  43307  rfovcnvf1od  43966  ntrneineine0lem  44045  funbrafv2b  47074  dfafn5a  47075  prprelb  47390