Theorem pm4.71rd 572

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  reueubd  3388  2reu5  3723  ralss  4011  rexss  4012  ralssOLD  4013  rexssOLD  4014  eqrrabd  4041  rabsneq  4610  reuhypd  5392  exopxfr2  5832  dfco2a  6249  onunel  6472  feu  6758  fcnvres  6759  funbrfv2b  6942  dffn5  6943  feqmptdf  6955  fimarab  6959  eqfnfv2  7030  dff4  7100  fmptco  7129  dff13  7257  opiota  8062  mpoxopovel  8222  brtpos  8237  dftpos3  8246  erinxp  8795  qliftfun  8806  pw2f1olem  9076  elirrv  9566  infm3  12191  indpi1  12249  prime  12695  predfz  13700  hashf1lem2  14513  hashle2prv  14535  oddnn02np1  16430  oddge22np1  16431  evennn02n  16432  evennn2n  16433  smueqlem  16572  vdwmc2  17063  acsfiel  17734  subsubc  17934  ismgmid  18750  eqger  19292  eqgid  19294  ghmqusker  19403  gaorber  19424  symgfix2  19532  rspsn0  21424  isfieldidl  21438  znleval  21756  psrbaglefi  22128  bastop2  23203  elcls2  23283  maxlp  23356  restopn2  23386  restdis  23387  1stccn  23673  tx1cn  23819  tx2cn  23820  imasnopn  23900  imasncld  23901  imasncls  23902  idqtop  23916  tgqtop  23922  filuni  24095  uffix2  24134  cnflf  24212  isfcls  24219  fclsopn  24224  cnfcf  24252  ptcmplem2  24263  xmeter  24643  imasf1oxms  24699  prdsbl  24701  caucfil  25495  cfilucfil4  25533  shft2rab  25720  sca2rab  25724  mbfinf  25877  i1f1lem  25901  i1fres  25917  itg1climres  25926  mbfi1fseqlem4  25930  iblpos  26005  itgposval  26008  cnplimc  26099  ply1remlem  26375  plyremlem  26518  dvdsflsumcom  27405  fsumvma2  27431  vmasum  27433  logfac2  27434  chpchtsum  27436  logfaclbnd  27439  lgsquadlem1  27597  lgsquadlem2  27598  lgsquadlem3  27599  dchrisum0lem1  27733  colinearalg  29317  nbusgreledg  29763  nbusgredgeu0  29778  umgr2v2enb1  29936  iswwlksnx  30258  wspniunwspnon  30341  clwlknf1oclwwlknlem2  30502  clwlknf1oclwwlkn  30504  eupth2lem2  30643  eupth2lems  30662  frgrncvvdeqlem2  30724  fusgr2wsp2nb  30758  fusgreg2wsp  30760  pjpreeq  31823  elnlfn  32353  nfpconfp  33050  fmptcof2  33075  dfcnv2  33093  2ndpreima  33126  f1od2  33136  fpwrelmap  33150  iocinioc2  33196  nndiffz1  33203  algextdeglem6  34178  1stmbfm  34717  2ndmbfm  34718  eulerpartlemgh  34835  bnj1171  35455  mrsubrn  36044  elfuns  36444  fneval  36922  mh-regprimbi  37115  bj-imdirval3  37887  topdifinfindis  38051  uncf  38309  phpreu  38314  poimirlem23  38353  poimirlem26  38356  poimirlem27  38357  areacirclem5  38422  erimeq2  39472  prter3  39716  islshpat  39851  lfl1dim  39955  glbconxN  40212  cdlemefrs29bpre0  41230  dib1dim  41999  dib1dim2  42002  diclspsn  42028  dihopelvalcpre  42082  dih1dimatlem  42163  mapdordlem1a  42468  hdmapoc  42765  prjspeclsp  43404  rmydioph  43801  pw2f1ocnv  43824  onsupeqnmax  44034  orddif0suc  44055  cantnf2  44112  tfsconcat0i  44132  rfovcnvf1od  44790  ntrneineine0lem  44869  modelaxreplem3  45749  funbrafv2b  47956  dfafn5a  47957  prprelb  48325  stgredgiun  48783  gpgiedgdmel  48874  gpgedgel  48875