Theorem pm4.71rd 562

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  reueubd  3360  2reu5  3705  ralss  3997  rexss  3998  ralssOLD  3999  rexssOLD  4000  eqrrabd  4027  rabsneq  4587  reuhypd  5357  exopxfr2  5794  dfco2a  6205  onunel  6425  feu  6711  fcnvres  6712  funbrfv2b  6892  dffn5  6893  feqmptdf  6905  fimarab  6909  eqfnfv2  6979  dff4  7048  fmptco  7077  dff13  7203  opiota  8006  mpoxopovel  8164  brtpos  8179  dftpos3  8188  erinxp  8732  qliftfun  8743  pw2f1olem  9013  infm3  12109  indpi1  12167  prime  12604  predfz  13601  hashf1lem2  14412  hashle2prv  14434  oddnn02np1  16311  oddge22np1  16312  evennn02n  16313  evennn2n  16314  smueqlem  16453  vdwmc2  16944  acsfiel  17614  subsubc  17814  ismgmid  18627  eqger  19147  eqgid  19149  ghmqusker  19256  gaorber  19277  symgfix2  19385  znleval  21547  psrbaglefi  21919  bastop2  22972  elcls2  23052  maxlp  23125  restopn2  23155  restdis  23156  1stccn  23441  tx1cn  23587  tx2cn  23588  imasnopn  23668  imasncld  23669  imasncls  23670  idqtop  23684  tgqtop  23690  filuni  23863  uffix2  23902  cnflf  23980  isfcls  23987  fclsopn  23992  cnfcf  24020  ptcmplem2  24031  xmeter  24411  imasf1oxms  24467  prdsbl  24469  caucfil  25263  cfilucfil4  25301  shft2rab  25488  sca2rab  25492  mbfinf  25645  i1f1lem  25669  i1fres  25685  itg1climres  25694  mbfi1fseqlem4  25698  iblpos  25773  itgposval  25776  cnplimc  25867  ply1remlem  26143  plyremlem  26284  dvdsflsumcom  27168  fsumvma2  27194  vmasum  27196  logfac2  27197  chpchtsum  27199  logfaclbnd  27202  lgsquadlem1  27360  lgsquadlem2  27361  lgsquadlem3  27362  dchrisum0lem1  27496  colinearalg  28996  nbusgreledg  29439  nbusgredgeu0  29454  umgr2v2enb1  29613  iswwlksnx  29926  wspniunwspnon  30009  clwlknf1oclwwlknlem2  30170  clwlknf1oclwwlkn  30172  eupth2lem2  30307  eupth2lems  30326  frgrncvvdeqlem2  30388  fusgr2wsp2nb  30422  fusgreg2wsp  30424  pjpreeq  31487  elnlfn  32017  nfpconfp  32723  fmptcof2  32748  dfcnv2  32766  2ndpreima  32799  f1od2  32810  fpwrelmap  32824  iocinioc2  32870  nndiffz1  32877  algextdeglem6  33885  1stmbfm  34423  2ndmbfm  34424  eulerpartlemgh  34541  bnj1171  35161  mrsubrn  35714  elfuns  36114  fneval  36553  mh-regprimbi  36746  bj-imdirval3  37517  topdifinfindis  37679  uncf  37937  phpreu  37942  poimirlem23  37981  poimirlem26  37984  poimirlem27  37985  areacirclem5  38050  erimeq2  39101  prter3  39345  islshpat  39480  lfl1dim  39584  glbconxN  39841  cdlemefrs29bpre0  40859  dib1dim  41628  dib1dim2  41631  diclspsn  41657  dihopelvalcpre  41711  dih1dimatlem  41792  mapdordlem1a  42097  hdmapoc  42394  prjspeclsp  43062  rmydioph  43463  pw2f1ocnv  43486  onsupeqnmax  43696  orddif0suc  43717  cantnf2  43774  tfsconcat0i  43794  rfovcnvf1od  44452  ntrneineine0lem  44531  modelaxreplem3  45428  funbrafv2b  47622  dfafn5a  47623  prprelb  47991  stgredgiun  48449  gpgiedgdmel  48540  gpgedgel  48541