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  3363  2reu5  3712  ralss  4004  rexss  4005  ralssOLD  4006  rexssOLD  4007  eqrrabd  4033  rabsneq  4592  reuhypd  5355  exopxfr2  5783  dfco2a  6193  onunel  6413  feu  6699  fcnvres  6700  funbrfv2b  6879  dffn5  6880  feqmptdf  6892  fimarab  6896  eqfnfv2  6965  dff4  7034  fmptco  7062  dff13  7188  opiota  7991  mpoxopovel  8150  brtpos  8165  dftpos3  8174  erinxp  8715  qliftfun  8726  pw2f1olem  8994  infm3  12081  prime  12554  predfz  13553  hashf1lem2  14363  hashle2prv  14385  oddnn02np1  16259  oddge22np1  16260  evennn02n  16261  evennn2n  16262  smueqlem  16401  vdwmc2  16891  acsfiel  17560  subsubc  17760  ismgmid  18573  eqger  19090  eqgid  19092  ghmqusker  19199  gaorber  19220  symgfix2  19328  znleval  21491  psrbaglefi  21863  bastop2  22909  elcls2  22989  maxlp  23062  restopn2  23092  restdis  23093  1stccn  23378  tx1cn  23524  tx2cn  23525  imasnopn  23605  imasncld  23606  imasncls  23607  idqtop  23621  tgqtop  23627  filuni  23800  uffix2  23839  cnflf  23917  isfcls  23924  fclsopn  23929  cnfcf  23957  ptcmplem2  23968  xmeter  24348  imasf1oxms  24404  prdsbl  24406  caucfil  25210  cfilucfil4  25248  shft2rab  25436  sca2rab  25440  mbfinf  25593  i1f1lem  25617  i1fres  25633  itg1climres  25642  mbfi1fseqlem4  25646  iblpos  25721  itgposval  25724  cnplimc  25815  ply1remlem  26097  plyremlem  26239  dvdsflsumcom  27125  fsumvma2  27152  vmasum  27154  logfac2  27155  chpchtsum  27157  logfaclbnd  27160  lgsquadlem1  27318  lgsquadlem2  27319  lgsquadlem3  27320  dchrisum0lem1  27454  colinearalg  28888  nbusgreledg  29331  nbusgredgeu0  29346  umgr2v2enb1  29505  iswwlksnx  29818  wspniunwspnon  29901  clwlknf1oclwwlknlem2  30062  clwlknf1oclwwlkn  30064  eupth2lem2  30199  eupth2lems  30218  frgrncvvdeqlem2  30280  fusgr2wsp2nb  30314  fusgreg2wsp  30316  pjpreeq  31378  elnlfn  31908  nfpconfp  32614  fmptcof2  32639  dfcnv2  32658  2ndpreima  32689  f1od2  32702  fpwrelmap  32716  iocinioc2  32762  nndiffz1  32769  indpi1  32841  algextdeglem6  33735  1stmbfm  34273  2ndmbfm  34274  eulerpartlemgh  34391  bnj1171  35012  mrsubrn  35557  elfuns  35957  fneval  36396  bj-imdirval3  37228  topdifinfindis  37390  uncf  37649  phpreu  37654  poimirlem23  37693  poimirlem26  37696  poimirlem27  37697  areacirclem5  37762  erimeq2  38786  prter3  38991  islshpat  39126  lfl1dim  39230  glbconxN  39487  cdlemefrs29bpre0  40505  dib1dim  41274  dib1dim2  41277  diclspsn  41303  dihopelvalcpre  41357  dih1dimatlem  41438  mapdordlem1a  41743  hdmapoc  42040  prjspeclsp  42715  rmydioph  43117  pw2f1ocnv  43140  onsupeqnmax  43350  orddif0suc  43371  cantnf2  43428  tfsconcat0i  43448  rfovcnvf1od  44107  ntrneineine0lem  44186  modelaxreplem3  45083  funbrafv2b  47269  dfafn5a  47270  prprelb  47626  stgredgiun  48068  gpgiedgdmel  48159  gpgedgel  48160