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  3382  2reu5  3716  ralss  4004  rexss  4005  ralssOLD  4006  rexssOLD  4007  eqrrabd  4034  rabsneq  4603  reuhypd  5384  exopxfr2  5824  dfco2a  6242  onunel  6465  feu  6752  fcnvres  6753  funbrfv2b  6936  dffn5  6937  feqmptdf  6949  fimarab  6953  eqfnfv2  7024  dff4  7095  fmptco  7124  dff13  7252  opiota  8057  mpoxopovel  8219  brtpos  8234  dftpos3  8243  erinxp  8792  qliftfun  8803  uncf  8871  pw2f1olem  9080  elirrv  9570  infm3  12199  indpi1  12257  prime  12703  predfz  13709  hashf1lem2  14522  hashle2prv  14544  oddnn02np1  16439  oddge22np1  16440  evennn02n  16441  evennn2n  16442  smueqlem  16581  vdwmc2  17072  acsfiel  17743  subsubc  17943  ismgmid  18759  eqger  19304  eqgid  19306  ghmqusker  19415  gaorber  19436  symgfix2  19544  rspsn0  21436  isfieldidl  21450  znleval  21768  psrbaglefi  22142  bastop2  23220  elcls2  23300  maxlp  23373  restopn2  23403  restdis  23404  1stccn  23690  tx1cn  23836  tx2cn  23837  imasnopn  23917  imasncld  23918  imasncls  23919  idqtop  23933  tgqtop  23939  filuni  24112  uffix2  24151  cnflf  24229  isfcls  24236  fclsopn  24241  cnfcf  24269  ptcmplem2  24280  xmeter  24660  imasf1oxms  24716  prdsbl  24718  caucfil  25512  cfilucfil4  25550  shft2rab  25737  sca2rab  25741  mbfinf  25894  i1f1lem  25918  i1fres  25934  itg1climres  25943  mbfi1fseqlem4  25947  iblpos  26021  itgposval  26024  cnplimc  26115  ply1remlem  26391  plyremlem  26535  dvdsflsumcom  27425  fsumvma2  27451  vmasum  27453  logfac2  27454  chpchtsum  27456  logfaclbnd  27459  lgsquadlem1  27617  lgsquadlem2  27618  lgsquadlem3  27619  dchrisum0lem1  27753  colinearalg  29368  nbusgreledg  29814  nbusgredgeu0  29829  umgr2v2enb1  29987  iswwlksnx  30309  wspniunwspnon  30392  clwlknf1oclwwlknlem2  30553  clwlknf1oclwwlkn  30555  eupth2lem2  30700  eupth2lems  30719  frgrncvvdeqlem2  30781  fusgr2wsp2nb  30815  fusgreg2wsp  30817  pjpreeq  31880  elnlfn  32410  nfpconfp  33106  fmptcof2  33131  dfcnv2  33149  2ndpreima  33181  f1od2  33191  fpwrelmap  33205  iocinioc2  33251  nndiffz1  33258  algextdeglem6  34233  1stmbfm  34772  2ndmbfm  34773  eulerpartlemgh  34890  bnj1171  35510  mrsubrn  36093  elfuns  36493  fneval  36972  mh-regprimbi  37165  bj-imdirval3  37937  topdifinfindis  38101  phpreu  38359  poimirlem23  38393  poimirlem26  38396  poimirlem27  38397  areacirclem5  38462  erimeq2  39512  prter3  39756  islshpat  39891  lfl1dim  39995  glbconxN  40252  cdlemefrs29bpre0  41270  dib1dim  42039  dib1dim2  42042  diclspsn  42068  dihopelvalcpre  42122  dih1dimatlem  42203  mapdordlem1a  42508  hdmapoc  42805  prjspeclsp  43459  rmydioph  43856  pw2f1ocnv  43879  onsupeqnmax  44089  orddif0suc  44110  cantnf2  44167  tfsconcat0i  44187  rfovcnvf1od  44845  ntrneineine0lem  44924  modelaxreplem3  45804  funbrafv2b  48048  dfafn5a  48049  prprelb  48417  stgredgiun  48875  gpgiedgdmel  48966  gpgedgel  48967