Theorem pm4.71rd 572

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

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

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 402

This theorem is used by:  reueubd  3385  2reu5  3718  ralss  3985  rexss  3986  eqrrabd  4013  rabsneq  4602  reuhypd  5384  exopxfr2  5826  dfrn7  6071  dfco2a  6253  onunel  6476  feu  6766  fcnvres  6767  funbrfv2b  6950  dffn5  6951  feqmptdf  6963  fimarab  6967  eqfnfv2  7038  dff4  7109  fmptco  7138  dff13  7265  opiota  8078  f1od2  8118  mpoxopovel  8248  brtpos  8263  dftpos3  8272  erinxp  8823  qliftfun  8834  uncf  8902  pw2f1olem  9111  elirrv  9601  infm3  12286  indpi1  12344  prime  12790  predfz  13797  hashf1lem2  14611  hashle2prv  14633  oddnn02np1  16530  oddge22np1  16531  evennn02n  16532  evennn2n  16533  smueqlem  16672  vdwmc2  17169  acsfiel  17840  subsubc  18040  ismgmid  18857  eqger  19402  eqgid  19404  ghmqusker  19513  gaorber  19534  symgfix2  19642  rspsn0  21538  isfieldidl  21552  znleval  21872  psrbaglefi  22246  bastop2  23324  elcls2  23404  maxlp  23477  restopn2  23507  restdis  23508  1stccn  23794  tx1cn  23940  tx2cn  23941  imasnopn  24021  imasncld  24022  imasncls  24023  idqtop  24037  tgqtop  24043  filuni  24216  uffix2  24255  cnflf  24333  isfcls  24340  fclsopn  24345  cnfcf  24373  ptcmplem2  24384  xmeter  24764  imasf1oxms  24820  prdsbl  24822  caucfil  25616  cfilucfil4  25654  shft2rab  25841  sca2rab  25845  mbfinf  25998  i1f1lem  26022  i1fres  26038  itg1climres  26047  mbfi1fseqlem4  26051  iblpos  26125  itgposval  26128  cnplimc  26219  ply1remlem  26495  plyremlem  26637  dvdsflsumcom  27527  fsumvma2  27553  vmasum  27555  logfac2  27556  chpchtsum  27558  logfaclbnd  27561  lgsquadlem1  27719  lgsquadlem2  27720  lgsquadlem3  27721  dchrisum0lem1  27855  colinearalg  29500  nbusgreledg  29946  nbusgredgeu0  29961  umgr2v2enb1  30119  iswwlksnx  30441  wspniunwspnon  30524  clwlknf1oclwwlknlem2  30685  clwlknf1oclwwlkn  30687  eupth2lem2  30832  eupth2lems  30851  frgrncvvdeqlem2  30913  fusgr2wsp2nb  30947  fusgreg2wsp  30949  pjpreeq  32012  elnlfn  32542  nfpconfp  33280  fmptcof2  33305  dfcnv2  33323  2ndpreima  33355  fpwrelmap  33378  iocinioc2  33424  nndiffz1  33431  algextdeglem6  34407  1stmbfm  34945  2ndmbfm  34946  eulerpartlemgh  35063  bnj1171  35683  mrsubrn  36399  elfuns  36804  fneval  37267  mh-regprimbi  37460  bj-imdirval3  38245  topdifinfindis  38409  phpreu  38667  poimirlem23  38701  poimirlem26  38704  poimirlem27  38705  areacirclem5  38770  erimeq2  39835  prter3  40079  islshpat  40214  lfl1dim  40318  glbconxN  40575  cdlemefrs29bpre0  41593  dib1dim  42362  dib1dim2  42365  diclspsn  42391  dihopelvalcpre  42445  dih1dimatlem  42526  mapdordlem1a  42831  hdmapoc  43128  prjspeclsp  43780  rmydioph  44161  pw2f1ocnv  44184  onsupeqnmax  44389  orddif0suc  44410  cantnf2  44467  tfsconcat0i  44487  rfovcnvf1od  45144  ntrneineine0lem  45223  modelaxreplem3  46109  funbrafv2b  48368  dfafn5a  48369  prprelb  48737  stgredgiun  49195  gpgiedgdmel  49286  gpgedgel  49287