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  3399  2reu5  3764  ralss  4058  rexss  4059  ralssOLD  4060  rexssOLD  4061  eqrrabd  4086  rabsneq  4644  reuhypd  5419  exopxfr2  5855  dfco2a  6266  onunel  6489  feu  6784  fcnvres  6785  funbrfv2b  6966  dffn5  6967  feqmptdf  6979  fimarab  6983  eqfnfv2  7052  dff4  7121  fmptco  7149  dff13  7275  opiota  8084  mpoxopovel  8245  brtpos  8260  dftpos3  8269  erinxp  8831  qliftfun  8842  pw2f1olem  9116  infm3  12227  prime  12699  predfz  13693  hashf1lem2  14495  hashle2prv  14517  oddnn02np1  16385  oddge22np1  16386  evennn02n  16387  evennn2n  16388  smueqlem  16527  vdwmc2  17017  acsfiel  17697  subsubc  17898  ismgmid  18678  eqger  19196  eqgid  19198  ghmqusker  19305  gaorber  19326  symgfix2  19434  znleval  21573  psrbaglefi  21946  bastop2  23001  elcls2  23082  maxlp  23155  restopn2  23185  restdis  23186  1stccn  23471  tx1cn  23617  tx2cn  23618  imasnopn  23698  imasncld  23699  imasncls  23700  idqtop  23714  tgqtop  23720  filuni  23893  uffix2  23932  cnflf  24010  isfcls  24017  fclsopn  24022  cnfcf  24050  ptcmplem2  24061  xmeter  24443  imasf1oxms  24502  prdsbl  24504  caucfil  25317  cfilucfil4  25355  shft2rab  25543  sca2rab  25547  mbfinf  25700  i1f1lem  25724  i1fres  25740  itg1climres  25749  mbfi1fseqlem4  25753  iblpos  25828  itgposval  25831  cnplimc  25922  ply1remlem  26204  plyremlem  26346  dvdsflsumcom  27231  fsumvma2  27258  vmasum  27260  logfac2  27261  chpchtsum  27263  logfaclbnd  27266  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  dchrisum0lem1  27560  colinearalg  28925  nbusgreledg  29370  nbusgredgeu0  29385  umgr2v2enb1  29544  iswwlksnx  29860  wspniunwspnon  29943  clwlknf1oclwwlknlem2  30101  clwlknf1oclwwlkn  30103  eupth2lem2  30238  eupth2lems  30257  frgrncvvdeqlem2  30319  fusgr2wsp2nb  30353  fusgreg2wsp  30355  pjpreeq  31417  elnlfn  31947  nfpconfp  32642  fmptcof2  32667  dfcnv2  32686  2ndpreima  32717  f1od2  32732  fpwrelmap  32744  iocinioc2  32781  nndiffz1  32788  indpi1  32845  algextdeglem6  33763  1stmbfm  34262  2ndmbfm  34263  eulerpartlemgh  34380  bnj1171  35014  mrsubrn  35518  elfuns  35916  fneval  36353  bj-imdirval3  37185  topdifinfindis  37347  uncf  37606  phpreu  37611  poimirlem23  37650  poimirlem26  37653  poimirlem27  37654  areacirclem5  37719  erimeq2  38679  prter3  38883  islshpat  39018  lfl1dim  39122  glbconxN  39380  cdlemefrs29bpre0  40398  dib1dim  41167  dib1dim2  41170  diclspsn  41196  dihopelvalcpre  41250  dih1dimatlem  41331  mapdordlem1a  41636  hdmapoc  41933  prjspeclsp  42622  rmydioph  43026  pw2f1ocnv  43049  onsupeqnmax  43259  orddif0suc  43281  cantnf2  43338  tfsconcat0i  43358  rfovcnvf1od  44017  ntrneineine0lem  44096  modelaxreplem3  44997  funbrafv2b  47171  dfafn5a  47172  prprelb  47503  stgredgiun  47925  gpgedgel  48007