Theorem pm4.71rd 567

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 566	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	2	biancomd 464	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  reueubd  3361  2reu5  3699  ralss  3987  rexss  3988  ralssOLD  3989  rexssOLD  3990  eqrrabd  4017  rabsneq  4574  reuhypd  5348  exopxfr2  5786  dfco2a  6197  onunel  6417  feu  6703  fcnvres  6704  funbrfv2b  6884  dffn5  6885  feqmptdf  6897  fimarab  6901  eqfnfv2  6972  dff4  7042  fmptco  7071  dff13  7198  opiota  8001  mpoxopovel  8160  brtpos  8175  dftpos3  8184  erinxp  8728  qliftfun  8739  pw2f1olem  9009  elirrv  9502  infm3  12106  indpi1  12164  prime  12601  predfz  13598  hashf1lem2  14409  hashle2prv  14431  oddnn02np1  16308  oddge22np1  16309  evennn02n  16310  evennn2n  16311  smueqlem  16450  vdwmc2  16941  acsfiel  17611  subsubc  17811  ismgmid  18624  eqger  19144  eqgid  19146  ghmqusker  19253  gaorber  19274  symgfix2  19382  znleval  21529  psrbaglefi  21901  bastop2  22977  elcls2  23057  maxlp  23130  restopn2  23160  restdis  23161  1stccn  23446  tx1cn  23592  tx2cn  23593  imasnopn  23673  imasncld  23674  imasncls  23675  idqtop  23689  tgqtop  23695  filuni  23868  uffix2  23907  cnflf  23985  isfcls  23992  fclsopn  23997  cnfcf  24025  ptcmplem2  24036  xmeter  24416  imasf1oxms  24472  prdsbl  24474  caucfil  25268  cfilucfil4  25306  shft2rab  25493  sca2rab  25497  mbfinf  25650  i1f1lem  25674  i1fres  25690  itg1climres  25699  mbfi1fseqlem4  25703  iblpos  25778  itgposval  25781  cnplimc  25872  ply1remlem  26148  plyremlem  26288  dvdsflsumcom  27169  fsumvma2  27195  vmasum  27197  logfac2  27198  chpchtsum  27200  logfaclbnd  27203  lgsquadlem1  27361  lgsquadlem2  27362  lgsquadlem3  27363  dchrisum0lem1  27497  colinearalg  28997  nbusgreledg  29440  nbusgredgeu0  29455  umgr2v2enb1  29613  iswwlksnx  29926  wspniunwspnon  30009  clwlknf1oclwwlknlem2  30170  clwlknf1oclwwlkn  30172  eupth2lem2  30307  eupth2lems  30326  frgrncvvdeqlem2  30388  fusgr2wsp2nb  30422  fusgreg2wsp  30424  pjpreeq  31487  elnlfn  32017  nfpconfp  32724  fmptcof2  32749  dfcnv2  32767  2ndpreima  32800  f1od2  32811  fpwrelmap  32825  iocinioc2  32871  nndiffz1  32878  algextdeglem6  33906  1stmbfm  34444  2ndmbfm  34445  eulerpartlemgh  34562  bnj1171  35182  mrsubrn  35741  elfuns  36141  fneval  36580  mh-regprimbi  36773  bj-imdirval3  37544  topdifinfindis  37708  uncf  37966  phpreu  37971  poimirlem23  38010  poimirlem26  38013  poimirlem27  38014  areacirclem5  38079  erimeq2  39130  prter3  39374  islshpat  39509  lfl1dim  39613  glbconxN  39870  cdlemefrs29bpre0  40888  dib1dim  41657  dib1dim2  41660  diclspsn  41686  dihopelvalcpre  41740  dih1dimatlem  41821  mapdordlem1a  42126  hdmapoc  42423  prjspeclsp  43062  rmydioph  43459  pw2f1ocnv  43482  onsupeqnmax  43692  orddif0suc  43713  cantnf2  43770  tfsconcat0i  43790  rfovcnvf1od  44448  ntrneineine0lem  44527  modelaxreplem3  45424  funbrafv2b  47622  dfafn5a  47623  prprelb  47991  stgredgiun  48449  gpgiedgdmel  48540  gpgedgel  48541