Theorem pm4.71rd 571

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  reueubd  3386  2reu5  3721  ralss  4010  rexss  4011  ralssOLD  4012  rexssOLD  4013  eqrrabd  4040  rabsneq  4608  reuhypd  5390  exopxfr2  5830  dfco2a  6247  onunel  6468  feu  6754  fcnvres  6755  funbrfv2b  6938  dffn5  6939  feqmptdf  6951  fimarab  6955  eqfnfv2  7026  dff4  7096  fmptco  7125  dff13  7252  opiota  8052  mpoxopovel  8212  brtpos  8227  dftpos3  8236  erinxp  8785  qliftfun  8796  pw2f1olem  9065  elirrv  9555  infm3  12169  indpi1  12227  prime  12672  predfz  13677  hashf1lem2  14489  hashle2prv  14511  oddnn02np1  16401  oddge22np1  16402  evennn02n  16403  evennn2n  16404  smueqlem  16543  vdwmc2  17034  acsfiel  17705  subsubc  17905  ismgmid  18718  eqger  19241  eqgid  19243  ghmqusker  19352  gaorber  19373  symgfix2  19481  rspsn0  21372  isfieldidl  21386  znleval  21704  psrbaglefi  22076  bastop2  23151  elcls2  23231  maxlp  23304  restopn2  23334  restdis  23335  1stccn  23620  tx1cn  23766  tx2cn  23767  imasnopn  23847  imasncld  23848  imasncls  23849  idqtop  23863  tgqtop  23869  filuni  24042  uffix2  24081  cnflf  24159  isfcls  24166  fclsopn  24171  cnfcf  24199  ptcmplem2  24210  xmeter  24590  imasf1oxms  24646  prdsbl  24648  caucfil  25442  cfilucfil4  25480  shft2rab  25667  sca2rab  25671  mbfinf  25824  i1f1lem  25848  i1fres  25864  itg1climres  25873  mbfi1fseqlem4  25877  iblpos  25952  itgposval  25955  cnplimc  26046  ply1remlem  26322  plyremlem  26465  dvdsflsumcom  27352  fsumvma2  27378  vmasum  27380  logfac2  27381  chpchtsum  27383  logfaclbnd  27386  lgsquadlem1  27544  lgsquadlem2  27545  lgsquadlem3  27546  dchrisum0lem1  27680  colinearalg  29260  nbusgreledg  29703  nbusgredgeu0  29718  umgr2v2enb1  29876  iswwlksnx  30189  wspniunwspnon  30272  clwlknf1oclwwlknlem2  30433  clwlknf1oclwwlkn  30435  eupth2lem2  30570  eupth2lems  30589  frgrncvvdeqlem2  30651  fusgr2wsp2nb  30685  fusgreg2wsp  30687  pjpreeq  31750  elnlfn  32280  nfpconfp  32977  fmptcof2  33002  dfcnv2  33020  2ndpreima  33053  f1od2  33064  fpwrelmap  33078  iocinioc2  33124  nndiffz1  33131  algextdeglem6  34112  1stmbfm  34650  2ndmbfm  34651  eulerpartlemgh  34768  bnj1171  35388  mrsubrn  36005  elfuns  36405  fneval  36883  mh-regprimbi  37076  bj-imdirval3  37848  topdifinfindis  38012  uncf  38270  phpreu  38275  poimirlem23  38314  poimirlem26  38317  poimirlem27  38318  areacirclem5  38383  erimeq2  39432  prter3  39676  islshpat  39811  lfl1dim  39915  glbconxN  40172  cdlemefrs29bpre0  41190  dib1dim  41959  dib1dim2  41962  diclspsn  41988  dihopelvalcpre  42042  dih1dimatlem  42123  mapdordlem1a  42428  hdmapoc  42725  prjspeclsp  43364  rmydioph  43761  pw2f1ocnv  43784  onsupeqnmax  43994  orddif0suc  44015  cantnf2  44072  tfsconcat0i  44092  rfovcnvf1od  44750  ntrneineine0lem  44829  modelaxreplem3  45709  funbrafv2b  47916  dfafn5a  47917  prprelb  48285  stgredgiun  48743  gpgiedgdmel  48834  gpgedgel  48835