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  3359  2reu5  3704  ralss  3996  rexss  3997  ralssOLD  3998  rexssOLD  3999  eqrrabd  4026  rabsneq  4586  reuhypd  5361  exopxfr2  5799  dfco2a  6210  onunel  6430  feu  6716  fcnvres  6717  funbrfv2b  6897  dffn5  6898  feqmptdf  6910  fimarab  6914  eqfnfv2  6984  dff4  7053  fmptco  7082  dff13  7209  opiota  8012  mpoxopovel  8170  brtpos  8185  dftpos3  8194  erinxp  8738  qliftfun  8749  pw2f1olem  9019  infm3  12115  indpi1  12173  prime  12610  predfz  13607  hashf1lem2  14418  hashle2prv  14440  oddnn02np1  16317  oddge22np1  16318  evennn02n  16319  evennn2n  16320  smueqlem  16459  vdwmc2  16950  acsfiel  17620  subsubc  17820  ismgmid  18633  eqger  19153  eqgid  19155  ghmqusker  19262  gaorber  19283  symgfix2  19391  znleval  21534  psrbaglefi  21906  bastop2  22959  elcls2  23039  maxlp  23112  restopn2  23142  restdis  23143  1stccn  23428  tx1cn  23574  tx2cn  23575  imasnopn  23655  imasncld  23656  imasncls  23657  idqtop  23671  tgqtop  23677  filuni  23850  uffix2  23889  cnflf  23967  isfcls  23974  fclsopn  23979  cnfcf  24007  ptcmplem2  24018  xmeter  24398  imasf1oxms  24454  prdsbl  24456  caucfil  25250  cfilucfil4  25288  shft2rab  25475  sca2rab  25479  mbfinf  25632  i1f1lem  25656  i1fres  25672  itg1climres  25681  mbfi1fseqlem4  25685  iblpos  25760  itgposval  25763  cnplimc  25854  ply1remlem  26130  plyremlem  26270  dvdsflsumcom  27151  fsumvma2  27177  vmasum  27179  logfac2  27180  chpchtsum  27182  logfaclbnd  27185  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  dchrisum0lem1  27479  colinearalg  28979  nbusgreledg  29422  nbusgredgeu0  29437  umgr2v2enb1  29595  iswwlksnx  29908  wspniunwspnon  29991  clwlknf1oclwwlknlem2  30152  clwlknf1oclwwlkn  30154  eupth2lem2  30289  eupth2lems  30308  frgrncvvdeqlem2  30370  fusgr2wsp2nb  30404  fusgreg2wsp  30406  pjpreeq  31469  elnlfn  31999  nfpconfp  32705  fmptcof2  32730  dfcnv2  32748  2ndpreima  32781  f1od2  32792  fpwrelmap  32806  iocinioc2  32852  nndiffz1  32859  algextdeglem6  33866  1stmbfm  34404  2ndmbfm  34405  eulerpartlemgh  34522  bnj1171  35142  mrsubrn  35695  elfuns  36095  fneval  36534  mh-regprimbi  36727  bj-imdirval3  37498  topdifinfindis  37662  uncf  37920  phpreu  37925  poimirlem23  37964  poimirlem26  37967  poimirlem27  37968  areacirclem5  38033  erimeq2  39084  prter3  39328  islshpat  39463  lfl1dim  39567  glbconxN  39824  cdlemefrs29bpre0  40842  dib1dim  41611  dib1dim2  41614  diclspsn  41640  dihopelvalcpre  41694  dih1dimatlem  41775  mapdordlem1a  42080  hdmapoc  42377  prjspeclsp  43045  rmydioph  43442  pw2f1ocnv  43465  onsupeqnmax  43675  orddif0suc  43696  cantnf2  43753  tfsconcat0i  43773  rfovcnvf1od  44431  ntrneineine0lem  44510  modelaxreplem3  45407  funbrafv2b  47607  dfafn5a  47608  prprelb  47976  stgredgiun  48434  gpgiedgdmel  48525  gpgedgel  48526