Theorem pm4.71rd 566

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 400

This theorem is referenced by:  reueubd  3381  2reu5  3697  ralss  3985  rexss  3986  reuhypd  5285  exopxfr2  5679  dfco2a  6066  feu  6528  fcnvres  6530  funbrfv2b  6698  dffn5  6699  feqmptdf  6710  eqfnfv2  6780  dff4  6844  fmptco  6868  dff13  6991  opiota  7739  mpoxopovel  7869  brtpos  7884  dftpos3  7893  erinxp  8354  qliftfun  8365  pw2f1olem  8604  infm3  11587  prime  12051  predfz  13027  hashf1lem2  13810  hashle2prv  13832  oddnn02np1  15689  oddge22np1  15690  evennn02n  15691  evennn2n  15692  smueqlem  15829  vdwmc2  16305  acsfiel  16917  subsubc  17115  ismgmid  17867  eqger  18322  eqgid  18324  gaorber  18430  symgfix2  18536  znleval  20246  psrbaglefi  20610  bastop2  21599  elcls2  21679  maxlp  21752  restopn2  21782  restdis  21783  1stccn  22068  tx1cn  22214  tx2cn  22215  imasnopn  22295  imasncld  22296  imasncls  22297  idqtop  22311  tgqtop  22317  filuni  22490  uffix2  22529  cnflf  22607  isfcls  22614  fclsopn  22619  cnfcf  22647  ptcmplem2  22658  xmeter  23040  imasf1oxms  23096  prdsbl  23098  caucfil  23887  cfilucfil4  23925  shft2rab  24112  sca2rab  24116  mbfinf  24269  i1f1lem  24293  i1fres  24309  itg1climres  24318  mbfi1fseqlem4  24322  iblpos  24396  itgposval  24399  cnplimc  24490  ply1remlem  24763  plyremlem  24900  dvdsflsumcom  25773  fsumvma2  25798  vmasum  25800  logfac2  25801  chpchtsum  25803  logfaclbnd  25806  lgsquadlem1  25964  lgsquadlem2  25965  lgsquadlem3  25966  dchrisum0lem1  26100  colinearalg  26704  nbusgreledg  27143  nbusgredgeu0  27158  umgr2v2enb1  27316  iswwlksnx  27626  wspniunwspnon  27709  clwlknf1oclwwlknlem2  27867  clwlknf1oclwwlkn  27869  eupth2lem2  28004  eupth2lems  28023  frgrncvvdeqlem2  28085  fusgr2wsp2nb  28119  fusgreg2wsp  28121  pjpreeq  29181  elnlfn  29711  eqrrabd  30272  nfpconfp  30391  fimarab  30404  fmptcof2  30420  dfcnv2  30439  2ndpreima  30467  f1od2  30483  fpwrelmap  30495  iocinioc2  30528  nndiffz1  30535  indpi1  31389  1stmbfm  31628  2ndmbfm  31629  eulerpartlemgh  31746  bnj1171  32382  mrsubrn  32873  elfuns  33489  fneval  33813  bj-imdirval3  34599  topdifinfindis  34763  uncf  35036  phpreu  35041  poimirlem23  35080  poimirlem26  35083  poimirlem27  35084  areacirclem5  35149  erim2  36071  prter3  36178  islshpat  36313  lfl1dim  36417  glbconxN  36674  cdlemefrs29bpre0  37692  dib1dim  38461  dib1dim2  38464  diclspsn  38490  dihopelvalcpre  38544  dih1dimatlem  38625  mapdordlem1a  38930  hdmapoc  39227  prjspeclsp  39606  rmydioph  39955  pw2f1ocnv  39978  rfovcnvf1od  40705  ntrneineine0lem  40786  funbrafv2b  43715  dfafn5a  43716  prprelb  44033