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  3365  2reu5  3714  ralss  4006  rexss  4007  ralssOLD  4008  rexssOLD  4009  eqrrabd  4036  rabsneq  4597  reuhypd  5362  exopxfr2  5791  dfco2a  6202  onunel  6422  feu  6708  fcnvres  6709  funbrfv2b  6889  dffn5  6890  feqmptdf  6902  fimarab  6906  eqfnfv2  6975  dff4  7044  fmptco  7072  dff13  7198  opiota  8001  mpoxopovel  8160  brtpos  8175  dftpos3  8184  erinxp  8726  qliftfun  8737  pw2f1olem  9007  infm3  12099  prime  12571  predfz  13567  hashf1lem2  14377  hashle2prv  14399  oddnn02np1  16273  oddge22np1  16274  evennn02n  16275  evennn2n  16276  smueqlem  16415  vdwmc2  16905  acsfiel  17575  subsubc  17775  ismgmid  18588  eqger  19105  eqgid  19107  ghmqusker  19214  gaorber  19235  symgfix2  19343  znleval  21507  psrbaglefi  21880  bastop2  22936  elcls2  23016  maxlp  23089  restopn2  23119  restdis  23120  1stccn  23405  tx1cn  23551  tx2cn  23552  imasnopn  23632  imasncld  23633  imasncls  23634  idqtop  23648  tgqtop  23654  filuni  23827  uffix2  23866  cnflf  23944  isfcls  23951  fclsopn  23956  cnfcf  23984  ptcmplem2  23995  xmeter  24375  imasf1oxms  24431  prdsbl  24433  caucfil  25237  cfilucfil4  25275  shft2rab  25463  sca2rab  25467  mbfinf  25620  i1f1lem  25644  i1fres  25660  itg1climres  25669  mbfi1fseqlem4  25673  iblpos  25748  itgposval  25751  cnplimc  25842  ply1remlem  26124  plyremlem  26266  dvdsflsumcom  27152  fsumvma2  27179  vmasum  27181  logfac2  27182  chpchtsum  27184  logfaclbnd  27187  lgsquadlem1  27345  lgsquadlem2  27346  lgsquadlem3  27347  dchrisum0lem1  27481  colinearalg  28932  nbusgreledg  29375  nbusgredgeu0  29390  umgr2v2enb1  29549  iswwlksnx  29862  wspniunwspnon  29945  clwlknf1oclwwlknlem2  30106  clwlknf1oclwwlkn  30108  eupth2lem2  30243  eupth2lems  30262  frgrncvvdeqlem2  30324  fusgr2wsp2nb  30358  fusgreg2wsp  30360  pjpreeq  31422  elnlfn  31952  nfpconfp  32659  fmptcof2  32684  dfcnv2  32703  2ndpreima  32736  f1od2  32747  fpwrelmap  32761  iocinioc2  32808  nndiffz1  32815  indpi1  32890  algextdeglem6  33828  1stmbfm  34366  2ndmbfm  34367  eulerpartlemgh  34484  bnj1171  35105  mrsubrn  35656  elfuns  36056  fneval  36495  bj-imdirval3  37328  topdifinfindis  37490  uncf  37739  phpreu  37744  poimirlem23  37783  poimirlem26  37786  poimirlem27  37787  areacirclem5  37852  erimeq2  38876  prter3  39081  islshpat  39216  lfl1dim  39320  glbconxN  39577  cdlemefrs29bpre0  40595  dib1dim  41364  dib1dim2  41367  diclspsn  41393  dihopelvalcpre  41447  dih1dimatlem  41528  mapdordlem1a  41833  hdmapoc  42130  prjspeclsp  42797  rmydioph  43198  pw2f1ocnv  43221  onsupeqnmax  43431  orddif0suc  43452  cantnf2  43509  tfsconcat0i  43529  rfovcnvf1od  44187  ntrneineine0lem  44266  modelaxreplem3  45163  funbrafv2b  47347  dfafn5a  47348  prprelb  47704  stgredgiun  48146  gpgiedgdmel  48237  gpgedgel  48238