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  3393  2reu5  3730  ralss  4018  rexss  4019  ralssOLD  4020  rexssOLD  4021  eqrrabd  4048  rabsneq  4613  reuhypd  5391  exopxfr2  5831  dfco2a  6248  onunel  6469  feu  6755  fcnvres  6756  funbrfv2b  6939  dffn5  6940  feqmptdf  6952  fimarab  6956  eqfnfv2  7027  dff4  7097  fmptco  7126  dff13  7253  opiota  8056  mpoxopovel  8216  brtpos  8231  dftpos3  8240  erinxp  8789  qliftfun  8800  pw2f1olem  9069  elirrv  9559  infm3  12174  indpi1  12232  prime  12677  predfz  13681  hashf1lem2  14493  hashle2prv  14515  oddnn02np1  16406  oddge22np1  16407  evennn02n  16408  evennn2n  16409  smueqlem  16548  vdwmc2  17039  acsfiel  17710  subsubc  17910  ismgmid  18723  eqger  19246  eqgid  19248  ghmqusker  19357  gaorber  19378  symgfix2  19486  znleval  21673  psrbaglefi  22045  bastop2  23120  elcls2  23200  maxlp  23273  restopn2  23303  restdis  23304  1stccn  23589  tx1cn  23735  tx2cn  23736  imasnopn  23816  imasncld  23817  imasncls  23818  idqtop  23832  tgqtop  23838  filuni  24011  uffix2  24050  cnflf  24128  isfcls  24135  fclsopn  24140  cnfcf  24168  ptcmplem2  24179  xmeter  24559  imasf1oxms  24615  prdsbl  24617  caucfil  25411  cfilucfil4  25449  shft2rab  25636  sca2rab  25640  mbfinf  25793  i1f1lem  25817  i1fres  25833  itg1climres  25842  mbfi1fseqlem4  25846  iblpos  25921  itgposval  25924  cnplimc  26015  ply1remlem  26291  plyremlem  26434  dvdsflsumcom  27318  fsumvma2  27344  vmasum  27346  logfac2  27347  chpchtsum  27349  logfaclbnd  27352  lgsquadlem1  27510  lgsquadlem2  27511  lgsquadlem3  27512  dchrisum0lem1  27646  colinearalg  29201  nbusgreledg  29644  nbusgredgeu0  29659  umgr2v2enb1  29817  iswwlksnx  30130  wspniunwspnon  30213  clwlknf1oclwwlknlem2  30374  clwlknf1oclwwlkn  30376  eupth2lem2  30511  eupth2lems  30530  frgrncvvdeqlem2  30592  fusgr2wsp2nb  30626  fusgreg2wsp  30628  pjpreeq  31691  elnlfn  32221  nfpconfp  32918  fmptcof2  32943  dfcnv2  32961  2ndpreima  32994  f1od2  33005  fpwrelmap  33019  iocinioc2  33065  nndiffz1  33072  algextdeglem6  34057  1stmbfm  34595  2ndmbfm  34596  eulerpartlemgh  34713  bnj1171  35333  mrsubrn  35904  elfuns  36304  fneval  36752  mh-regprimbi  36945  bj-imdirval3  37716  topdifinfindis  37880  uncf  38138  phpreu  38143  poimirlem23  38182  poimirlem26  38185  poimirlem27  38186  areacirclem5  38251  erimeq2  39302  prter3  39546  islshpat  39681  lfl1dim  39785  glbconxN  40042  cdlemefrs29bpre0  41060  dib1dim  41829  dib1dim2  41832  diclspsn  41858  dihopelvalcpre  41912  dih1dimatlem  41993  mapdordlem1a  42298  hdmapoc  42595  prjspeclsp  43236  rmydioph  43633  pw2f1ocnv  43656  onsupeqnmax  43866  orddif0suc  43887  cantnf2  43944  tfsconcat0i  43964  rfovcnvf1od  44622  ntrneineine0lem  44701  modelaxreplem3  45581  funbrafv2b  47785  dfafn5a  47786  prprelb  48154  stgredgiun  48612  gpgiedgdmel  48703  gpgedgel  48704