Theorem pm4.71rd 563

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  reueubd  3395  2reu5  3754  ralss  4054  rexss  4055  reuhypd  5417  exopxfr2  5844  dfco2a  6245  onunel  6469  feu  6767  fcnvres  6768  funbrfv2b  6949  dffn5  6950  feqmptdf  6962  eqfnfv2  7033  dff4  7102  fmptco  7129  dff13  7256  opiota  8047  mpoxopovel  8207  brtpos  8222  dftpos3  8231  erinxp  8787  qliftfun  8798  pw2f1olem  9078  infm3  12175  prime  12645  predfz  13628  hashf1lem2  14419  hashle2prv  14441  oddnn02np1  16293  oddge22np1  16294  evennn02n  16295  evennn2n  16296  smueqlem  16433  vdwmc2  16914  acsfiel  17600  subsubc  17805  ismgmid  18586  eqger  19060  eqgid  19062  gaorber  19174  symgfix2  19286  znleval  21116  psrbaglefi  21491  psrbaglefiOLD  21492  bastop2  22504  elcls2  22585  maxlp  22658  restopn2  22688  restdis  22689  1stccn  22974  tx1cn  23120  tx2cn  23121  imasnopn  23201  imasncld  23202  imasncls  23203  idqtop  23217  tgqtop  23223  filuni  23396  uffix2  23435  cnflf  23513  isfcls  23520  fclsopn  23525  cnfcf  23553  ptcmplem2  23564  xmeter  23946  imasf1oxms  24005  prdsbl  24007  caucfil  24807  cfilucfil4  24845  shft2rab  25032  sca2rab  25036  mbfinf  25189  i1f1lem  25213  i1fres  25230  itg1climres  25239  mbfi1fseqlem4  25243  iblpos  25317  itgposval  25320  cnplimc  25411  ply1remlem  25687  plyremlem  25824  dvdsflsumcom  26699  fsumvma2  26724  vmasum  26726  logfac2  26727  chpchtsum  26729  logfaclbnd  26732  lgsquadlem1  26890  lgsquadlem2  26891  lgsquadlem3  26892  dchrisum0lem1  27026  colinearalg  28206  nbusgreledg  28648  nbusgredgeu0  28663  umgr2v2enb1  28821  iswwlksnx  29132  wspniunwspnon  29215  clwlknf1oclwwlknlem2  29373  clwlknf1oclwwlkn  29375  eupth2lem2  29510  eupth2lems  29529  frgrncvvdeqlem2  29591  fusgr2wsp2nb  29625  fusgreg2wsp  29627  pjpreeq  30689  elnlfn  31219  eqrrabd  31779  nfpconfp  31894  fimarab  31906  fmptcof2  31920  dfcnv2  31939  2ndpreima  31967  f1od2  31984  fpwrelmap  31996  iocinioc2  32028  nndiffz1  32035  ghmqusker  32577  algextdeglem6  32838  indpi1  33087  1stmbfm  33328  2ndmbfm  33329  eulerpartlemgh  33446  bnj1171  34080  mrsubrn  34573  elfuns  34956  fneval  35323  bj-imdirval3  36151  topdifinfindis  36313  uncf  36553  phpreu  36558  poimirlem23  36597  poimirlem26  36600  poimirlem27  36601  areacirclem5  36666  erimeq2  37634  prter3  37838  islshpat  37973  lfl1dim  38077  glbconxN  38335  cdlemefrs29bpre0  39353  dib1dim  40122  dib1dim2  40125  diclspsn  40151  dihopelvalcpre  40205  dih1dimatlem  40286  mapdordlem1a  40591  hdmapoc  40888  prjspeclsp  41436  rmydioph  41835  pw2f1ocnv  41858  onsupeqnmax  42078  orddif0suc  42100  cantnf2  42157  tfsconcat0i  42177  rfovcnvf1od  42837  ntrneineine0lem  42916  funbrafv2b  45946  dfafn5a  45947  prprelb  46263