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  3367  2reu5  3693  ralss  3991  rexss  3992  reuhypd  5342  exopxfr2  5753  dfco2a  6150  feu  6650  fcnvres  6651  funbrfv2b  6827  dffn5  6828  feqmptdf  6839  eqfnfv2  6910  dff4  6977  fmptco  7001  dff13  7128  opiota  7899  mpoxopovel  8036  brtpos  8051  dftpos3  8060  erinxp  8580  qliftfun  8591  pw2f1olem  8863  infm3  11934  prime  12401  predfz  13381  hashf1lem2  14170  hashle2prv  14192  oddnn02np1  16057  oddge22np1  16058  evennn02n  16059  evennn2n  16060  smueqlem  16197  vdwmc2  16680  acsfiel  17363  subsubc  17568  ismgmid  18349  eqger  18806  eqgid  18808  gaorber  18914  symgfix2  19024  znleval  20762  psrbaglefi  21135  psrbaglefiOLD  21136  bastop2  22144  elcls2  22225  maxlp  22298  restopn2  22328  restdis  22329  1stccn  22614  tx1cn  22760  tx2cn  22761  imasnopn  22841  imasncld  22842  imasncls  22843  idqtop  22857  tgqtop  22863  filuni  23036  uffix2  23075  cnflf  23153  isfcls  23160  fclsopn  23165  cnfcf  23193  ptcmplem2  23204  xmeter  23586  imasf1oxms  23645  prdsbl  23647  caucfil  24447  cfilucfil4  24485  shft2rab  24672  sca2rab  24676  mbfinf  24829  i1f1lem  24853  i1fres  24870  itg1climres  24879  mbfi1fseqlem4  24883  iblpos  24957  itgposval  24960  cnplimc  25051  ply1remlem  25327  plyremlem  25464  dvdsflsumcom  26337  fsumvma2  26362  vmasum  26364  logfac2  26365  chpchtsum  26367  logfaclbnd  26370  lgsquadlem1  26528  lgsquadlem2  26529  lgsquadlem3  26530  dchrisum0lem1  26664  colinearalg  27278  nbusgreledg  27720  nbusgredgeu0  27735  umgr2v2enb1  27893  iswwlksnx  28205  wspniunwspnon  28288  clwlknf1oclwwlknlem2  28446  clwlknf1oclwwlkn  28448  eupth2lem2  28583  eupth2lems  28602  frgrncvvdeqlem2  28664  fusgr2wsp2nb  28698  fusgreg2wsp  28700  pjpreeq  29760  elnlfn  30290  eqrrabd  30849  nfpconfp  30967  fimarab  30980  fmptcof2  30994  dfcnv2  31013  2ndpreima  31040  f1od2  31056  fpwrelmap  31068  iocinioc2  31100  nndiffz1  31107  indpi1  31988  1stmbfm  32227  2ndmbfm  32228  eulerpartlemgh  32345  bnj1171  32980  mrsubrn  33475  onunel  33689  elfuns  34217  fneval  34541  bj-imdirval3  35355  topdifinfindis  35517  uncf  35756  phpreu  35761  poimirlem23  35800  poimirlem26  35803  poimirlem27  35804  areacirclem5  35869  erim2  36789  prter3  36896  islshpat  37031  lfl1dim  37135  glbconxN  37392  cdlemefrs29bpre0  38410  dib1dim  39179  dib1dim2  39182  diclspsn  39208  dihopelvalcpre  39262  dih1dimatlem  39343  mapdordlem1a  39648  hdmapoc  39945  prjspeclsp  40451  rmydioph  40836  pw2f1ocnv  40859  rfovcnvf1od  41612  ntrneineine0lem  41693  funbrafv2b  44651  dfafn5a  44652  prprelb  44968