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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  reueubd  3357  2reu5  3688  ralss  3987  rexss  3988  reuhypd  5337  exopxfr2  5742  dfco2a  6139  feu  6634  fcnvres  6635  funbrfv2b  6809  dffn5  6810  feqmptdf  6821  eqfnfv2  6892  dff4  6959  fmptco  6983  dff13  7109  opiota  7872  mpoxopovel  8007  brtpos  8022  dftpos3  8031  erinxp  8538  qliftfun  8549  pw2f1olem  8816  infm3  11864  prime  12331  predfz  13310  hashf1lem2  14098  hashle2prv  14120  oddnn02np1  15985  oddge22np1  15986  evennn02n  15987  evennn2n  15988  smueqlem  16125  vdwmc2  16608  acsfiel  17280  subsubc  17484  ismgmid  18264  eqger  18721  eqgid  18723  gaorber  18829  symgfix2  18939  znleval  20674  psrbaglefi  21045  psrbaglefiOLD  21046  bastop2  22052  elcls2  22133  maxlp  22206  restopn2  22236  restdis  22237  1stccn  22522  tx1cn  22668  tx2cn  22669  imasnopn  22749  imasncld  22750  imasncls  22751  idqtop  22765  tgqtop  22771  filuni  22944  uffix2  22983  cnflf  23061  isfcls  23068  fclsopn  23073  cnfcf  23101  ptcmplem2  23112  xmeter  23494  imasf1oxms  23551  prdsbl  23553  caucfil  24352  cfilucfil4  24390  shft2rab  24577  sca2rab  24581  mbfinf  24734  i1f1lem  24758  i1fres  24775  itg1climres  24784  mbfi1fseqlem4  24788  iblpos  24862  itgposval  24865  cnplimc  24956  ply1remlem  25232  plyremlem  25369  dvdsflsumcom  26242  fsumvma2  26267  vmasum  26269  logfac2  26270  chpchtsum  26272  logfaclbnd  26275  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  dchrisum0lem1  26569  colinearalg  27181  nbusgreledg  27623  nbusgredgeu0  27638  umgr2v2enb1  27796  iswwlksnx  28106  wspniunwspnon  28189  clwlknf1oclwwlknlem2  28347  clwlknf1oclwwlkn  28349  eupth2lem2  28484  eupth2lems  28503  frgrncvvdeqlem2  28565  fusgr2wsp2nb  28599  fusgreg2wsp  28601  pjpreeq  29661  elnlfn  30191  eqrrabd  30750  nfpconfp  30868  fimarab  30881  fmptcof2  30896  dfcnv2  30915  2ndpreima  30942  f1od2  30958  fpwrelmap  30970  iocinioc2  31002  nndiffz1  31009  indpi1  31888  1stmbfm  32127  2ndmbfm  32128  eulerpartlemgh  32245  bnj1171  32880  mrsubrn  33375  onunel  33592  elfuns  34144  fneval  34468  bj-imdirval3  35282  topdifinfindis  35444  uncf  35683  phpreu  35688  poimirlem23  35727  poimirlem26  35730  poimirlem27  35731  areacirclem5  35796  erim2  36716  prter3  36823  islshpat  36958  lfl1dim  37062  glbconxN  37319  cdlemefrs29bpre0  38337  dib1dim  39106  dib1dim2  39109  diclspsn  39135  dihopelvalcpre  39189  dih1dimatlem  39270  mapdordlem1a  39575  hdmapoc  39872  prjspeclsp  40372  rmydioph  40752  pw2f1ocnv  40775  rfovcnvf1od  41501  ntrneineine0lem  41582  funbrafv2b  44538  dfafn5a  44539  prprelb  44856