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  3378  2reu5  3741  ralss  4033  rexss  4034  ralssOLD  4035  rexssOLD  4036  eqrrabd  4061  rabsneq  4620  reuhypd  5389  exopxfr2  5824  dfco2a  6235  onunel  6459  feu  6754  fcnvres  6755  funbrfv2b  6936  dffn5  6937  feqmptdf  6949  fimarab  6953  eqfnfv2  7022  dff4  7091  fmptco  7119  dff13  7247  opiota  8058  mpoxopovel  8219  brtpos  8234  dftpos3  8243  erinxp  8805  qliftfun  8816  pw2f1olem  9090  infm3  12201  prime  12674  predfz  13670  hashf1lem2  14474  hashle2prv  14496  oddnn02np1  16367  oddge22np1  16368  evennn02n  16369  evennn2n  16370  smueqlem  16509  vdwmc2  16999  acsfiel  17666  subsubc  17866  ismgmid  18643  eqger  19161  eqgid  19163  ghmqusker  19270  gaorber  19291  symgfix2  19397  znleval  21515  psrbaglefi  21886  bastop2  22932  elcls2  23012  maxlp  23085  restopn2  23115  restdis  23116  1stccn  23401  tx1cn  23547  tx2cn  23548  imasnopn  23628  imasncld  23629  imasncls  23630  idqtop  23644  tgqtop  23650  filuni  23823  uffix2  23862  cnflf  23940  isfcls  23947  fclsopn  23952  cnfcf  23980  ptcmplem2  23991  xmeter  24372  imasf1oxms  24428  prdsbl  24430  caucfil  25235  cfilucfil4  25273  shft2rab  25461  sca2rab  25465  mbfinf  25618  i1f1lem  25642  i1fres  25658  itg1climres  25667  mbfi1fseqlem4  25671  iblpos  25746  itgposval  25749  cnplimc  25840  ply1remlem  26122  plyremlem  26264  dvdsflsumcom  27150  fsumvma2  27177  vmasum  27179  logfac2  27180  chpchtsum  27182  logfaclbnd  27185  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  dchrisum0lem1  27479  colinearalg  28889  nbusgreledg  29332  nbusgredgeu0  29347  umgr2v2enb1  29506  iswwlksnx  29822  wspniunwspnon  29905  clwlknf1oclwwlknlem2  30063  clwlknf1oclwwlkn  30065  eupth2lem2  30200  eupth2lems  30219  frgrncvvdeqlem2  30281  fusgr2wsp2nb  30315  fusgreg2wsp  30317  pjpreeq  31379  elnlfn  31909  nfpconfp  32610  fmptcof2  32635  dfcnv2  32654  2ndpreima  32685  f1od2  32698  fpwrelmap  32710  iocinioc2  32756  nndiffz1  32763  indpi1  32837  algextdeglem6  33756  1stmbfm  34292  2ndmbfm  34293  eulerpartlemgh  34410  bnj1171  35031  mrsubrn  35535  elfuns  35933  fneval  36370  bj-imdirval3  37202  topdifinfindis  37364  uncf  37623  phpreu  37628  poimirlem23  37667  poimirlem26  37670  poimirlem27  37671  areacirclem5  37736  erimeq2  38696  prter3  38900  islshpat  39035  lfl1dim  39139  glbconxN  39397  cdlemefrs29bpre0  40415  dib1dim  41184  dib1dim2  41187  diclspsn  41213  dihopelvalcpre  41267  dih1dimatlem  41348  mapdordlem1a  41653  hdmapoc  41950  prjspeclsp  42635  rmydioph  43038  pw2f1ocnv  43061  onsupeqnmax  43271  orddif0suc  43292  cantnf2  43349  tfsconcat0i  43369  rfovcnvf1od  44028  ntrneineine0lem  44107  modelaxreplem3  45005  funbrafv2b  47188  dfafn5a  47189  prprelb  47530  stgredgiun  47970  gpgiedgdmel  48053  gpgedgel  48054