Theorem pm4.71rd 561

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 560	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	2	biancomd 462	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  reueubd  3382  2reu5  3751  ralss  4053  rexss  4054  rabsneq  4650  reuhypd  5422  exopxfr2  5850  dfco2a  6256  onunel  6480  feu  6777  fcnvres  6778  funbrfv2b  6959  dffn5  6960  feqmptdf  6972  eqfnfv2  7044  dff4  7114  fmptco  7142  dff13  7269  opiota  8072  mpoxopovel  8234  brtpos  8249  dftpos3  8258  erinxp  8819  qliftfun  8830  pw2f1olem  9113  infm3  12220  prime  12690  predfz  13675  hashf1lem2  14470  hashle2prv  14492  oddnn02np1  16345  oddge22np1  16346  evennn02n  16347  evennn2n  16348  smueqlem  16485  vdwmc2  16976  acsfiel  17662  subsubc  17867  ismgmid  18653  eqger  19167  eqgid  19169  ghmqusker  19276  gaorber  19297  symgfix2  19409  znleval  21544  psrbaglefi  21921  psrbaglefiOLD  21922  bastop2  22980  elcls2  23061  maxlp  23134  restopn2  23164  restdis  23165  1stccn  23450  tx1cn  23596  tx2cn  23597  imasnopn  23677  imasncld  23678  imasncls  23679  idqtop  23693  tgqtop  23699  filuni  23872  uffix2  23911  cnflf  23989  isfcls  23996  fclsopn  24001  cnfcf  24029  ptcmplem2  24040  xmeter  24422  imasf1oxms  24481  prdsbl  24483  caucfil  25294  cfilucfil4  25332  shft2rab  25520  sca2rab  25524  mbfinf  25677  i1f1lem  25701  i1fres  25718  itg1climres  25727  mbfi1fseqlem4  25731  iblpos  25805  itgposval  25808  cnplimc  25899  ply1remlem  26184  plyremlem  26324  dvdsflsumcom  27208  fsumvma2  27235  vmasum  27237  logfac2  27238  chpchtsum  27240  logfaclbnd  27243  lgsquadlem1  27401  lgsquadlem2  27402  lgsquadlem3  27403  dchrisum0lem1  27537  colinearalg  28836  nbusgreledg  29281  nbusgredgeu0  29296  umgr2v2enb1  29455  iswwlksnx  29766  wspniunwspnon  29849  clwlknf1oclwwlknlem2  30007  clwlknf1oclwwlkn  30009  eupth2lem2  30144  eupth2lems  30163  frgrncvvdeqlem2  30225  fusgr2wsp2nb  30259  fusgreg2wsp  30261  pjpreeq  31323  elnlfn  31853  eqrrabd  32420  nfpconfp  32540  fimarab  32551  fmptcof2  32565  dfcnv2  32584  2ndpreima  32610  f1od2  32626  fpwrelmap  32638  iocinioc2  32670  nndiffz1  32677  algextdeglem6  33559  indpi1  33809  1stmbfm  34050  2ndmbfm  34051  eulerpartlemgh  34168  bnj1171  34801  mrsubrn  35293  elfuns  35687  fneval  36012  bj-imdirval3  36839  topdifinfindis  37001  uncf  37248  phpreu  37253  poimirlem23  37292  poimirlem26  37295  poimirlem27  37296  areacirclem5  37361  erimeq2  38324  prter3  38528  islshpat  38663  lfl1dim  38767  glbconxN  39025  cdlemefrs29bpre0  40043  dib1dim  40812  dib1dim2  40815  diclspsn  40841  dihopelvalcpre  40895  dih1dimatlem  40976  mapdordlem1a  41281  hdmapoc  41578  prjspeclsp  42203  rmydioph  42609  pw2f1ocnv  42632  onsupeqnmax  42849  orddif0suc  42871  cantnf2  42928  tfsconcat0i  42948  rfovcnvf1od  43608  ntrneineine0lem  43687  funbrafv2b  46709  dfafn5a  46710  prprelb  47025