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  3369  2reu5  3718  ralss  4010  rexss  4011  ralssOLD  4012  rexssOLD  4013  eqrrabd  4040  rabsneq  4601  reuhypd  5366  exopxfr2  5801  dfco2a  6212  onunel  6432  feu  6718  fcnvres  6719  funbrfv2b  6899  dffn5  6900  feqmptdf  6912  fimarab  6916  eqfnfv2  6986  dff4  7055  fmptco  7084  dff13  7210  opiota  8013  mpoxopovel  8172  brtpos  8187  dftpos3  8196  erinxp  8740  qliftfun  8751  pw2f1olem  9021  infm3  12113  prime  12585  predfz  13581  hashf1lem2  14391  hashle2prv  14413  oddnn02np1  16287  oddge22np1  16288  evennn02n  16289  evennn2n  16290  smueqlem  16429  vdwmc2  16919  acsfiel  17589  subsubc  17789  ismgmid  18602  eqger  19119  eqgid  19121  ghmqusker  19228  gaorber  19249  symgfix2  19357  znleval  21521  psrbaglefi  21894  bastop2  22950  elcls2  23030  maxlp  23103  restopn2  23133  restdis  23134  1stccn  23419  tx1cn  23565  tx2cn  23566  imasnopn  23646  imasncld  23647  imasncls  23648  idqtop  23662  tgqtop  23668  filuni  23841  uffix2  23880  cnflf  23958  isfcls  23965  fclsopn  23970  cnfcf  23998  ptcmplem2  24009  xmeter  24389  imasf1oxms  24445  prdsbl  24447  caucfil  25251  cfilucfil4  25289  shft2rab  25477  sca2rab  25481  mbfinf  25634  i1f1lem  25658  i1fres  25674  itg1climres  25683  mbfi1fseqlem4  25687  iblpos  25762  itgposval  25765  cnplimc  25856  ply1remlem  26138  plyremlem  26280  dvdsflsumcom  27166  fsumvma2  27193  vmasum  27195  logfac2  27196  chpchtsum  27198  logfaclbnd  27201  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  dchrisum0lem1  27495  colinearalg  28995  nbusgreledg  29438  nbusgredgeu0  29453  umgr2v2enb1  29612  iswwlksnx  29925  wspniunwspnon  30008  clwlknf1oclwwlknlem2  30169  clwlknf1oclwwlkn  30171  eupth2lem2  30306  eupth2lems  30325  frgrncvvdeqlem2  30387  fusgr2wsp2nb  30421  fusgreg2wsp  30423  pjpreeq  31486  elnlfn  32016  nfpconfp  32722  fmptcof2  32747  dfcnv2  32765  2ndpreima  32798  f1od2  32809  fpwrelmap  32823  iocinioc2  32870  nndiffz1  32877  indpi1  32952  algextdeglem6  33900  1stmbfm  34438  2ndmbfm  34439  eulerpartlemgh  34556  bnj1171  35176  mrsubrn  35729  elfuns  36129  fneval  36568  bj-imdirval3  37439  topdifinfindis  37601  uncf  37850  phpreu  37855  poimirlem23  37894  poimirlem26  37897  poimirlem27  37898  areacirclem5  37963  erimeq2  39014  prter3  39258  islshpat  39393  lfl1dim  39497  glbconxN  39754  cdlemefrs29bpre0  40772  dib1dim  41541  dib1dim2  41544  diclspsn  41570  dihopelvalcpre  41624  dih1dimatlem  41705  mapdordlem1a  42010  hdmapoc  42307  prjspeclsp  42970  rmydioph  43371  pw2f1ocnv  43394  onsupeqnmax  43604  orddif0suc  43625  cantnf2  43682  tfsconcat0i  43702  rfovcnvf1od  44360  ntrneineine0lem  44439  modelaxreplem3  45336  funbrafv2b  47519  dfafn5a  47520  prprelb  47876  stgredgiun  48318  gpgiedgdmel  48409  gpgedgel  48410