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  3367  2reu5  3716  ralss  4008  rexss  4009  ralssOLD  4010  rexssOLD  4011  eqrrabd  4038  rabsneq  4599  reuhypd  5364  exopxfr2  5793  dfco2a  6204  onunel  6424  feu  6710  fcnvres  6711  funbrfv2b  6891  dffn5  6892  feqmptdf  6904  fimarab  6908  eqfnfv2  6977  dff4  7046  fmptco  7074  dff13  7200  opiota  8003  mpoxopovel  8162  brtpos  8177  dftpos3  8186  erinxp  8728  qliftfun  8739  pw2f1olem  9009  infm3  12101  prime  12573  predfz  13569  hashf1lem2  14379  hashle2prv  14401  oddnn02np1  16275  oddge22np1  16276  evennn02n  16277  evennn2n  16278  smueqlem  16417  vdwmc2  16907  acsfiel  17577  subsubc  17777  ismgmid  18590  eqger  19107  eqgid  19109  ghmqusker  19216  gaorber  19237  symgfix2  19345  znleval  21509  psrbaglefi  21882  bastop2  22938  elcls2  23018  maxlp  23091  restopn2  23121  restdis  23122  1stccn  23407  tx1cn  23553  tx2cn  23554  imasnopn  23634  imasncld  23635  imasncls  23636  idqtop  23650  tgqtop  23656  filuni  23829  uffix2  23868  cnflf  23946  isfcls  23953  fclsopn  23958  cnfcf  23986  ptcmplem2  23997  xmeter  24377  imasf1oxms  24433  prdsbl  24435  caucfil  25239  cfilucfil4  25277  shft2rab  25465  sca2rab  25469  mbfinf  25622  i1f1lem  25646  i1fres  25662  itg1climres  25671  mbfi1fseqlem4  25675  iblpos  25750  itgposval  25753  cnplimc  25844  ply1remlem  26126  plyremlem  26268  dvdsflsumcom  27154  fsumvma2  27181  vmasum  27183  logfac2  27184  chpchtsum  27186  logfaclbnd  27189  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  dchrisum0lem1  27483  colinearalg  28983  nbusgreledg  29426  nbusgredgeu0  29441  umgr2v2enb1  29600  iswwlksnx  29913  wspniunwspnon  29996  clwlknf1oclwwlknlem2  30157  clwlknf1oclwwlkn  30159  eupth2lem2  30294  eupth2lems  30313  frgrncvvdeqlem2  30375  fusgr2wsp2nb  30409  fusgreg2wsp  30411  pjpreeq  31473  elnlfn  32003  nfpconfp  32710  fmptcof2  32735  dfcnv2  32754  2ndpreima  32787  f1od2  32798  fpwrelmap  32812  iocinioc2  32859  nndiffz1  32866  indpi1  32941  algextdeglem6  33879  1stmbfm  34417  2ndmbfm  34418  eulerpartlemgh  34535  bnj1171  35156  mrsubrn  35707  elfuns  36107  fneval  36546  bj-imdirval3  37389  topdifinfindis  37551  uncf  37800  phpreu  37805  poimirlem23  37844  poimirlem26  37847  poimirlem27  37848  areacirclem5  37913  erimeq2  38947  prter3  39152  islshpat  39287  lfl1dim  39391  glbconxN  39648  cdlemefrs29bpre0  40666  dib1dim  41435  dib1dim2  41438  diclspsn  41464  dihopelvalcpre  41518  dih1dimatlem  41599  mapdordlem1a  41904  hdmapoc  42201  prjspeclsp  42865  rmydioph  43266  pw2f1ocnv  43289  onsupeqnmax  43499  orddif0suc  43520  cantnf2  43577  tfsconcat0i  43597  rfovcnvf1od  44255  ntrneineine0lem  44334  modelaxreplem3  45231  funbrafv2b  47415  dfafn5a  47416  prprelb  47772  stgredgiun  48214  gpgiedgdmel  48305  gpgedgel  48306