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  3373  2reu5  3729  ralss  4021  rexss  4022  ralssOLD  4023  rexssOLD  4024  eqrrabd  4049  rabsneq  4608  reuhypd  5374  exopxfr2  5808  dfco2a  6219  onunel  6439  feu  6736  fcnvres  6737  funbrfv2b  6918  dffn5  6919  feqmptdf  6931  fimarab  6935  eqfnfv2  7004  dff4  7073  fmptco  7101  dff13  7229  opiota  8038  mpoxopovel  8199  brtpos  8214  dftpos3  8223  erinxp  8764  qliftfun  8775  pw2f1olem  9045  infm3  12142  prime  12615  predfz  13614  hashf1lem2  14421  hashle2prv  14443  oddnn02np1  16318  oddge22np1  16319  evennn02n  16320  evennn2n  16321  smueqlem  16460  vdwmc2  16950  acsfiel  17615  subsubc  17815  ismgmid  18592  eqger  19110  eqgid  19112  ghmqusker  19219  gaorber  19240  symgfix2  19346  znleval  21464  psrbaglefi  21835  bastop2  22881  elcls2  22961  maxlp  23034  restopn2  23064  restdis  23065  1stccn  23350  tx1cn  23496  tx2cn  23497  imasnopn  23577  imasncld  23578  imasncls  23579  idqtop  23593  tgqtop  23599  filuni  23772  uffix2  23811  cnflf  23889  isfcls  23896  fclsopn  23901  cnfcf  23929  ptcmplem2  23940  xmeter  24321  imasf1oxms  24377  prdsbl  24379  caucfil  25183  cfilucfil4  25221  shft2rab  25409  sca2rab  25413  mbfinf  25566  i1f1lem  25590  i1fres  25606  itg1climres  25615  mbfi1fseqlem4  25619  iblpos  25694  itgposval  25697  cnplimc  25788  ply1remlem  26070  plyremlem  26212  dvdsflsumcom  27098  fsumvma2  27125  vmasum  27127  logfac2  27128  chpchtsum  27130  logfaclbnd  27133  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  dchrisum0lem1  27427  colinearalg  28837  nbusgreledg  29280  nbusgredgeu0  29295  umgr2v2enb1  29454  iswwlksnx  29770  wspniunwspnon  29853  clwlknf1oclwwlknlem2  30011  clwlknf1oclwwlkn  30013  eupth2lem2  30148  eupth2lems  30167  frgrncvvdeqlem2  30229  fusgr2wsp2nb  30263  fusgreg2wsp  30265  pjpreeq  31327  elnlfn  31857  nfpconfp  32556  fmptcof2  32581  dfcnv2  32600  2ndpreima  32631  f1od2  32644  fpwrelmap  32656  iocinioc2  32702  nndiffz1  32709  indpi1  32783  algextdeglem6  33712  1stmbfm  34251  2ndmbfm  34252  eulerpartlemgh  34369  bnj1171  34990  mrsubrn  35500  elfuns  35903  fneval  36340  bj-imdirval3  37172  topdifinfindis  37334  uncf  37593  phpreu  37598  poimirlem23  37637  poimirlem26  37640  poimirlem27  37641  areacirclem5  37706  erimeq2  38670  prter3  38875  islshpat  39010  lfl1dim  39114  glbconxN  39372  cdlemefrs29bpre0  40390  dib1dim  41159  dib1dim2  41162  diclspsn  41188  dihopelvalcpre  41242  dih1dimatlem  41323  mapdordlem1a  41628  hdmapoc  41925  prjspeclsp  42600  rmydioph  43003  pw2f1ocnv  43026  onsupeqnmax  43236  orddif0suc  43257  cantnf2  43314  tfsconcat0i  43334  rfovcnvf1od  43993  ntrneineine0lem  44072  modelaxreplem3  44970  funbrafv2b  47160  dfafn5a  47161  prprelb  47517  stgredgiun  47957  gpgiedgdmel  48040  gpgedgel  48041