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  3386  2reu5  3719  ralss  3986  rexss  3987  eqrrabd  4014  rabsneq  4603  reuhypd  5388  exopxfr2  5832  dfrn7  6084  dfco2a  6266  onunel  6496  feu  6788  fcnvres  6789  funbrfv2b  6973  dffn5  6974  feqmptdf  6986  fimarab  6990  eqfnfv2  7061  elpreima  7088  dff4  7133  fmptco  7162  dff13  7289  opiota  8105  f1od2  8145  mpoxopovel  8275  brtpos  8290  dftpos3  8299  erinxp  8850  qliftfun  8861  uncf  8929  pw2f1olem  9138  elirrv  9628  infm3  12316  indpi1  12374  prime  12820  predfz  13827  hashf1lem2  14642  hashle2prv  14664  oddnn02np1  16562  oddge22np1  16563  evennn02n  16564  evennn2n  16565  smueqlem  16704  vdwmc2  17201  acsfiel  17878  subsubc  18078  ismgmid  18895  eqger  19440  eqgid  19442  ghmqusker  19552  gaorber  19573  symgfix2  19681  rspsn0  21577  isfieldidl  21591  znleval  21915  psrbaglefi  22289  bastop2  23367  elcls2  23447  maxlp  23520  restopn2  23550  restdis  23551  1stccn  23837  tx1cn  23983  tx2cn  23984  imasnopn  24064  imasncld  24065  imasncls  24066  idqtop  24080  tgqtop  24086  filuni  24259  uffix2  24298  cnflf  24376  isfcls  24383  fclsopn  24388  cnfcf  24416  ptcmplem2  24427  xmeter  24807  imasf1oxms  24863  prdsbl  24865  caucfil  25659  cfilucfil4  25697  shft2rab  25884  sca2rab  25888  mbfinf  26041  i1f1lem  26065  i1fres  26081  itg1climres  26090  mbfi1fseqlem4  26094  iblpos  26168  itgposval  26171  cnplimc  26262  ply1remlem  26538  plyremlem  26680  dvdsflsumcom  27572  fsumvma2  27598  vmasum  27600  logfac2  27601  chpchtsum  27603  logfaclbnd  27606  lgsquadlem1  27764  lgsquadlem2  27765  lgsquadlem3  27766  dchrisum0lem1  27900  colinearalg  29545  nbusgreledg  29991  nbusgredgeu0  30006  umgr2v2enb1  30164  iswwlksnx  30486  wspniunwspnon  30569  clwlknf1oclwwlknlem2  30730  clwlknf1oclwwlkn  30732  eupth2lem2  30877  eupth2lems  30896  frgrncvvdeqlem2  30958  fusgr2wsp2nb  30992  fusgreg2wsp  30994  pjpreeq  32057  elnlfn  32587  nfpconfp  33324  fmptcof2  33349  dfcnv2  33366  2ndpreima  33398  fpwrelmap  33421  iocinioc2  33467  nndiffz1  33474  algextdeglem6  34465  1stmbfm  35003  2ndmbfm  35004  eulerpartlemgh  35121  bnj1171  35741  mrsubrn  36486  elfuns  36892  fneval  37355  mh-regprimbi  37548  bj-imdirval3  38373  topdifinfindis  38537  phpreu  38795  poimirlem23  38829  poimirlem26  38832  poimirlem27  38833  areacirclem5  38898  erimeq2  39961  prter3  40205  islshpat  40340  lfl1dim  40444  glbconxN  40701  cdlemefrs29bpre0  41719  dib1dim  42488  dib1dim2  42491  diclspsn  42517  dihopelvalcpre  42571  dih1dimatlem  42652  mapdordlem1a  42957  hdmapoc  43254  prjspeclsp  43906  rmydioph  44287  pw2f1ocnv  44310  onsupeqnmax  44510  orddif0suc  44531  cantnf2  44588  tfsconcat0i  44608  rfovcnvf1od  45265  ntrneineine0lem  45344  modelaxreplem3  46234  funbrafv2b  48502  dfafn5a  48503  prprelb  48871  stgredgiun  49329  gpgiedgdmel  49420  gpgedgel  49421