Theorem pm4.71rd 667

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	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
pm4.71rd	|- ( ph -> ( ps <-> ( ch /\ ps ) ) )

Proof of Theorem pm4.71rd

Step	Hyp	Ref	Expression
1		pm4.71rd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		pm4.71r 663	. 2 |- ( ( ps -> ch ) <-> ( ps <-> ( ch /\ ps ) ) )
3	1, 2	sylib 208	1 |- ( ph -> ( ps <-> ( ch /\ ps ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  reueubd  3164  2reu5  3416  ralss  3668  rexss  3669  reuhypd  4895  exopxfr2  5266  dfco2a  5635  feu  6080  funbrfv2b  6240  dffn5  6241  feqmptdf  6251  eqfnfv2  6312  dff4  6373  fmptco  6396  dff13  6512  opiota  7229  mpt2xopovel  7346  brtpos  7361  dftpos3  7370  erinxp  7821  qliftfun  7832  pw2f1olem  8064  infm3  10982  prime  11458  predfz  12464  hashf1lem2  13240  hashle2prv  13260  oddnn02np1  15072  oddge22np1  15073  evennn02n  15074  evennn2n  15075  smueqlem  15212  vdwmc2  15683  acsfiel  16315  subsubc  16513  ismgmid  17264  eqger  17644  eqgid  17646  gaorber  17741  symgfix2  17836  psrbaglefi  19372  znleval  19903  bastop2  20798  elcls2  20878  maxlp  20951  restopn2  20981  restdis  20982  1stccn  21266  tx1cn  21412  tx2cn  21413  imasnopn  21493  imasncld  21494  imasncls  21495  idqtop  21509  tgqtop  21515  filuni  21689  uffix2  21728  cnflf  21806  isfcls  21813  fclsopn  21818  cnfcf  21846  ptcmplem2  21857  xmeter  22238  imasf1oxms  22294  prdsbl  22296  caucfil  23081  cfilucfil4  23118  shft2rab  23276  sca2rab  23280  mbfinf  23432  i1f1lem  23456  i1fres  23472  itg1climres  23481  mbfi1fseqlem4  23485  iblpos  23559  itgposval  23562  cnplimc  23651  ply1remlem  23922  plyremlem  24059  dvdsflsumcom  24914  fsumvma2  24939  vmasum  24941  logfac2  24942  chpchtsum  24944  logfaclbnd  24947  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  dchrisum0lem1  25205  colinearalg  25790  nbgrel  26238  nbusgreledg  26249  nbusgredgeu0  26270  umgr2v2enb1  26422  iswwlksnx  26731  wspniunwspnon  26819  eupth2lem2  27079  eupth2lems  27098  frgrncvvdeqlem2  27164  fusgr2wsp2nb  27198  fusgreg2wsp  27200  pjpreeq  28257  elnlfn  28787  fimarab  29445  fmptcof2  29457  dfcnv2  29476  2ndpreima  29485  f1od2  29499  fpwrelmap  29508  iocinioc2  29541  nndiffz1  29548  indpi1  30082  1stmbfm  30322  2ndmbfm  30323  eulerpartlemgh  30440  bnj1171  31068  mrsubrn  31410  elfuns  32022  fneval  32347  topdifinfindis  33194  uncf  33388  phpreu  33393  poimirlem23  33432  poimirlem26  33435  poimirlem27  33436  areacirclem5  33504  prter3  34167  islshpat  34304  lfl1dim  34408  glbconxN  34664  cdlemefrs29bpre0  35684  dib1dim  36454  dib1dim2  36457  diclspsn  36483  dihopelvalcpre  36537  dih1dimatlem  36618  mapdordlem1a  36923  hdmapoc  37223  rmydioph  37581  pw2f1ocnv  37604  rfovcnvf1od  38298  ntrneineine0lem  38381  funbrafv2b  41239  dfafn5a  41240