Theorem pm4.71rd 571

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

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 401

This theorem is used by:  reueubd  3385  2reu5  3720  ralss  4009  rexss  4010  ralssOLD  4011  rexssOLD  4012  eqrrabd  4039  rabsneq  4607  reuhypd  5389  exopxfr2  5829  dfco2a  6246  onunel  6468  feu  6754  fcnvres  6755  funbrfv2b  6938  dffn5  6939  feqmptdf  6951  fimarab  6955  eqfnfv2  7026  dff4  7096  fmptco  7125  dff13  7252  opiota  8054  mpoxopovel  8214  brtpos  8229  dftpos3  8238  erinxp  8787  qliftfun  8798  pw2f1olem  9067  elirrv  9557  infm3  12180  indpi1  12238  prime  12683  predfz  13688  hashf1lem2  14500  hashle2prv  14522  oddnn02np1  16412  oddge22np1  16413  evennn02n  16414  evennn2n  16415  smueqlem  16554  vdwmc2  17045  acsfiel  17716  subsubc  17916  ismgmid  18729  eqger  19252  eqgid  19254  ghmqusker  19363  gaorber  19384  symgfix2  19492  rspsn0  21383  isfieldidl  21397  znleval  21715  psrbaglefi  22087  bastop2  23162  elcls2  23242  maxlp  23315  restopn2  23345  restdis  23346  1stccn  23631  tx1cn  23777  tx2cn  23778  imasnopn  23858  imasncld  23859  imasncls  23860  idqtop  23874  tgqtop  23880  filuni  24053  uffix2  24092  cnflf  24170  isfcls  24177  fclsopn  24182  cnfcf  24210  ptcmplem2  24221  xmeter  24601  imasf1oxms  24657  prdsbl  24659  caucfil  25453  cfilucfil4  25491  shft2rab  25678  sca2rab  25682  mbfinf  25835  i1f1lem  25859  i1fres  25875  itg1climres  25884  mbfi1fseqlem4  25888  iblpos  25963  itgposval  25966  cnplimc  26057  ply1remlem  26333  plyremlem  26476  dvdsflsumcom  27363  fsumvma2  27389  vmasum  27391  logfac2  27392  chpchtsum  27394  logfaclbnd  27397  lgsquadlem1  27555  lgsquadlem2  27556  lgsquadlem3  27557  dchrisum0lem1  27691  colinearalg  29271  nbusgreledg  29714  nbusgredgeu0  29729  umgr2v2enb1  29887  iswwlksnx  30200  wspniunwspnon  30283  clwlknf1oclwwlknlem2  30444  clwlknf1oclwwlkn  30446  eupth2lem2  30581  eupth2lems  30600  frgrncvvdeqlem2  30662  fusgr2wsp2nb  30696  fusgreg2wsp  30698  pjpreeq  31761  elnlfn  32291  nfpconfp  32988  fmptcof2  33013  dfcnv2  33031  2ndpreima  33064  f1od2  33075  fpwrelmap  33089  iocinioc2  33135  nndiffz1  33142  algextdeglem6  34121  1stmbfm  34659  2ndmbfm  34660  eulerpartlemgh  34777  bnj1171  35397  mrsubrn  36013  elfuns  36413  fneval  36891  mh-regprimbi  37084  bj-imdirval3  37856  topdifinfindis  38020  uncf  38278  phpreu  38283  poimirlem23  38322  poimirlem26  38325  poimirlem27  38326  areacirclem5  38391  erimeq2  39440  prter3  39684  islshpat  39819  lfl1dim  39923  glbconxN  40180  cdlemefrs29bpre0  41198  dib1dim  41967  dib1dim2  41970  diclspsn  41996  dihopelvalcpre  42050  dih1dimatlem  42131  mapdordlem1a  42436  hdmapoc  42733  prjspeclsp  43372  rmydioph  43769  pw2f1ocnv  43792  onsupeqnmax  44002  orddif0suc  44023  cantnf2  44080  tfsconcat0i  44100  rfovcnvf1od  44758  ntrneineine0lem  44837  modelaxreplem3  45717  funbrafv2b  47924  dfafn5a  47925  prprelb  48293  stgredgiun  48751  gpgiedgdmel  48842  gpgedgel  48843