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  3375  2reu5  3732  ralss  4024  rexss  4025  ralssOLD  4026  rexssOLD  4027  eqrrabd  4052  rabsneq  4611  reuhypd  5377  exopxfr2  5811  dfco2a  6222  onunel  6442  feu  6739  fcnvres  6740  funbrfv2b  6921  dffn5  6922  feqmptdf  6934  fimarab  6938  eqfnfv2  7007  dff4  7076  fmptco  7104  dff13  7232  opiota  8041  mpoxopovel  8202  brtpos  8217  dftpos3  8226  erinxp  8767  qliftfun  8778  pw2f1olem  9050  infm3  12149  prime  12622  predfz  13621  hashf1lem2  14428  hashle2prv  14450  oddnn02np1  16325  oddge22np1  16326  evennn02n  16327  evennn2n  16328  smueqlem  16467  vdwmc2  16957  acsfiel  17622  subsubc  17822  ismgmid  18599  eqger  19117  eqgid  19119  ghmqusker  19226  gaorber  19247  symgfix2  19353  znleval  21471  psrbaglefi  21842  bastop2  22888  elcls2  22968  maxlp  23041  restopn2  23071  restdis  23072  1stccn  23357  tx1cn  23503  tx2cn  23504  imasnopn  23584  imasncld  23585  imasncls  23586  idqtop  23600  tgqtop  23606  filuni  23779  uffix2  23818  cnflf  23896  isfcls  23903  fclsopn  23908  cnfcf  23936  ptcmplem2  23947  xmeter  24328  imasf1oxms  24384  prdsbl  24386  caucfil  25190  cfilucfil4  25228  shft2rab  25416  sca2rab  25420  mbfinf  25573  i1f1lem  25597  i1fres  25613  itg1climres  25622  mbfi1fseqlem4  25626  iblpos  25701  itgposval  25704  cnplimc  25795  ply1remlem  26077  plyremlem  26219  dvdsflsumcom  27105  fsumvma2  27132  vmasum  27134  logfac2  27135  chpchtsum  27137  logfaclbnd  27140  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  dchrisum0lem1  27434  colinearalg  28844  nbusgreledg  29287  nbusgredgeu0  29302  umgr2v2enb1  29461  iswwlksnx  29777  wspniunwspnon  29860  clwlknf1oclwwlknlem2  30018  clwlknf1oclwwlkn  30020  eupth2lem2  30155  eupth2lems  30174  frgrncvvdeqlem2  30236  fusgr2wsp2nb  30270  fusgreg2wsp  30272  pjpreeq  31334  elnlfn  31864  nfpconfp  32563  fmptcof2  32588  dfcnv2  32607  2ndpreima  32638  f1od2  32651  fpwrelmap  32663  iocinioc2  32709  nndiffz1  32716  indpi1  32790  algextdeglem6  33719  1stmbfm  34258  2ndmbfm  34259  eulerpartlemgh  34376  bnj1171  34997  mrsubrn  35507  elfuns  35910  fneval  36347  bj-imdirval3  37179  topdifinfindis  37341  uncf  37600  phpreu  37605  poimirlem23  37644  poimirlem26  37647  poimirlem27  37648  areacirclem5  37713  erimeq2  38677  prter3  38882  islshpat  39017  lfl1dim  39121  glbconxN  39379  cdlemefrs29bpre0  40397  dib1dim  41166  dib1dim2  41169  diclspsn  41195  dihopelvalcpre  41249  dih1dimatlem  41330  mapdordlem1a  41635  hdmapoc  41932  prjspeclsp  42607  rmydioph  43010  pw2f1ocnv  43033  onsupeqnmax  43243  orddif0suc  43264  cantnf2  43321  tfsconcat0i  43341  rfovcnvf1od  44000  ntrneineine0lem  44079  modelaxreplem3  44977  funbrafv2b  47164  dfafn5a  47165  prprelb  47521  stgredgiun  47961  gpgiedgdmel  48044  gpgedgel  48045