Theorem pm4.71rd 570

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 569	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	2	biancomd 467	1 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  reueubd  3384  2reu5  3721  ralss  4009  rexss  4010  ralssOLD  4011  rexssOLD  4012  eqrrabd  4039  rabsneq  4601  reuhypd  5376  exopxfr2  5816  dfco2a  6233  onunel  6453  feu  6740  fcnvres  6741  funbrfv2b  6924  dffn5  6925  feqmptdf  6937  fimarab  6941  eqfnfv2  7012  dff4  7082  fmptco  7111  dff13  7238  opiota  8040  mpoxopovel  8200  brtpos  8215  dftpos3  8224  erinxp  8773  qliftfun  8784  pw2f1olem  9053  elirrv  9545  infm3  12151  indpi1  12209  prime  12654  predfz  13658  hashf1lem2  14469  hashle2prv  14491  oddnn02np1  16382  oddge22np1  16383  evennn02n  16384  evennn2n  16385  smueqlem  16524  vdwmc2  17015  acsfiel  17686  subsubc  17886  ismgmid  18699  eqger  19219  eqgid  19221  ghmqusker  19327  gaorber  19348  symgfix2  19456  znleval  21606  psrbaglefi  21978  bastop2  23054  elcls2  23134  maxlp  23207  restopn2  23237  restdis  23238  1stccn  23523  tx1cn  23669  tx2cn  23670  imasnopn  23750  imasncld  23751  imasncls  23752  idqtop  23766  tgqtop  23772  filuni  23945  uffix2  23984  cnflf  24062  isfcls  24069  fclsopn  24074  cnfcf  24102  ptcmplem2  24113  xmeter  24493  imasf1oxms  24549  prdsbl  24551  caucfil  25345  cfilucfil4  25383  shft2rab  25570  sca2rab  25574  mbfinf  25727  i1f1lem  25751  i1fres  25767  itg1climres  25776  mbfi1fseqlem4  25780  iblpos  25855  itgposval  25858  cnplimc  25949  ply1remlem  26225  plyremlem  26368  dvdsflsumcom  27252  fsumvma2  27278  vmasum  27280  logfac2  27281  chpchtsum  27283  logfaclbnd  27286  lgsquadlem1  27444  lgsquadlem2  27445  lgsquadlem3  27446  dchrisum0lem1  27580  colinearalg  29111  nbusgreledg  29554  nbusgredgeu0  29569  umgr2v2enb1  29727  iswwlksnx  30040  wspniunwspnon  30123  clwlknf1oclwwlknlem2  30284  clwlknf1oclwwlkn  30286  eupth2lem2  30421  eupth2lems  30440  frgrncvvdeqlem2  30502  fusgr2wsp2nb  30536  fusgreg2wsp  30538  pjpreeq  31601  elnlfn  32131  nfpconfp  32834  fmptcof2  32859  dfcnv2  32877  2ndpreima  32910  f1od2  32921  fpwrelmap  32935  iocinioc2  32981  nndiffz1  32988  algextdeglem6  34019  1stmbfm  34557  2ndmbfm  34558  eulerpartlemgh  34675  bnj1171  35295  mrsubrn  35863  elfuns  36263  fneval  36712  mh-regprimbi  36905  bj-imdirval3  37676  topdifinfindis  37840  uncf  38098  phpreu  38103  poimirlem23  38142  poimirlem26  38145  poimirlem27  38146  areacirclem5  38211  erimeq2  39262  prter3  39506  islshpat  39641  lfl1dim  39745  glbconxN  40002  cdlemefrs29bpre0  41020  dib1dim  41789  dib1dim2  41792  diclspsn  41818  dihopelvalcpre  41872  dih1dimatlem  41953  mapdordlem1a  42258  hdmapoc  42555  prjspeclsp  43194  rmydioph  43591  pw2f1ocnv  43614  onsupeqnmax  43824  orddif0suc  43845  cantnf2  43902  tfsconcat0i  43922  rfovcnvf1od  44580  ntrneineine0lem  44659  modelaxreplem3  45556  funbrafv2b  47753  dfafn5a  47754  prprelb  48122  stgredgiun  48580  gpgiedgdmel  48671  gpgedgel  48672