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  3362  2reu5  3718  ralss  4010  rexss  4011  ralssOLD  4012  rexssOLD  4013  eqrrabd  4037  rabsneq  4596  reuhypd  5358  exopxfr2  5787  dfco2a  6195  onunel  6414  feu  6700  fcnvres  6701  funbrfv2b  6880  dffn5  6881  feqmptdf  6893  fimarab  6897  eqfnfv2  6966  dff4  7035  fmptco  7063  dff13  7191  opiota  7994  mpoxopovel  8153  brtpos  8168  dftpos3  8177  erinxp  8718  qliftfun  8729  pw2f1olem  8998  infm3  12084  prime  12557  predfz  13556  hashf1lem2  14363  hashle2prv  14385  oddnn02np1  16259  oddge22np1  16260  evennn02n  16261  evennn2n  16262  smueqlem  16401  vdwmc2  16891  acsfiel  17560  subsubc  17760  ismgmid  18539  eqger  19057  eqgid  19059  ghmqusker  19166  gaorber  19187  symgfix2  19295  znleval  21461  psrbaglefi  21833  bastop2  22879  elcls2  22959  maxlp  23032  restopn2  23062  restdis  23063  1stccn  23348  tx1cn  23494  tx2cn  23495  imasnopn  23575  imasncld  23576  imasncls  23577  idqtop  23591  tgqtop  23597  filuni  23770  uffix2  23809  cnflf  23887  isfcls  23894  fclsopn  23899  cnfcf  23927  ptcmplem2  23938  xmeter  24319  imasf1oxms  24375  prdsbl  24377  caucfil  25181  cfilucfil4  25219  shft2rab  25407  sca2rab  25411  mbfinf  25564  i1f1lem  25588  i1fres  25604  itg1climres  25613  mbfi1fseqlem4  25617  iblpos  25692  itgposval  25695  cnplimc  25786  ply1remlem  26068  plyremlem  26210  dvdsflsumcom  27096  fsumvma2  27123  vmasum  27125  logfac2  27126  chpchtsum  27128  logfaclbnd  27131  lgsquadlem1  27289  lgsquadlem2  27290  lgsquadlem3  27291  dchrisum0lem1  27425  colinearalg  28855  nbusgreledg  29298  nbusgredgeu0  29313  umgr2v2enb1  29472  iswwlksnx  29785  wspniunwspnon  29868  clwlknf1oclwwlknlem2  30026  clwlknf1oclwwlkn  30028  eupth2lem2  30163  eupth2lems  30182  frgrncvvdeqlem2  30244  fusgr2wsp2nb  30278  fusgreg2wsp  30280  pjpreeq  31342  elnlfn  31872  nfpconfp  32575  fmptcof2  32600  dfcnv2  32619  2ndpreima  32650  f1od2  32663  fpwrelmap  32676  iocinioc2  32722  nndiffz1  32729  indpi1  32803  algextdeglem6  33689  1stmbfm  34228  2ndmbfm  34229  eulerpartlemgh  34346  bnj1171  34967  mrsubrn  35490  elfuns  35893  fneval  36330  bj-imdirval3  37162  topdifinfindis  37324  uncf  37583  phpreu  37588  poimirlem23  37627  poimirlem26  37630  poimirlem27  37631  areacirclem5  37696  erimeq2  38660  prter3  38865  islshpat  39000  lfl1dim  39104  glbconxN  39361  cdlemefrs29bpre0  40379  dib1dim  41148  dib1dim2  41151  diclspsn  41177  dihopelvalcpre  41231  dih1dimatlem  41312  mapdordlem1a  41617  hdmapoc  41914  prjspeclsp  42589  rmydioph  42991  pw2f1ocnv  43014  onsupeqnmax  43224  orddif0suc  43245  cantnf2  43302  tfsconcat0i  43322  rfovcnvf1od  43981  ntrneineine0lem  44060  modelaxreplem3  44958  funbrafv2b  47147  dfafn5a  47148  prprelb  47504  stgredgiun  47946  gpgiedgdmel  48037  gpgedgel  48038