Theorem pm4.71rd 628

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 624	. 2 |- ( ( ps -> ch ) <-> ( ps <-> ( ch /\ ps ) ) )
3	1, 2	sylib 196	1 |- ( ph -> ( ps <-> ( ch /\ ps ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  2reu5  3156  ralss  3406  rexss  3407  reuhypd  4507  exopxfr2  4971  dfco2a  5326  feu  5575  funbrfv2b  5724  dffn5  5725  eqfnfv2  5786  dff4  5845  fmptco  5863  dff13  5958  opiota  6622  mpt2xopovel  6726  brtpos  6743  dftpos3  6752  erinxp  7162  qliftfun  7173  pw2f1olem  7403  infm3  10277  prime  10710  hashf1lem2  12193  smueqlem  13669  vdwmc2  14023  acsfiel  14575  subsubc  14746  ismgmid  15418  eqger  15711  eqgid  15713  gaorber  15806  symgfix2  15901  psrbaglefi  17375  psrbaglefiOLD  17376  znleval  17829  bastop2  18441  elcls2  18520  maxlp  18593  restopn2  18623  restdis  18624  1stccn  18909  tx1cn  19024  tx2cn  19025  imasnopn  19105  imasncld  19106  imasncls  19107  idqtop  19121  tgqtop  19127  filuni  19300  uffix2  19339  cnflf  19417  isfcls  19424  fclsopn  19429  cnfcf  19457  ptcmplem2  19467  xmeter  19850  imasf1oxms  19906  prdsbl  19908  caucfil  20636  cfilucfil4OLD  20673  cfilucfil4  20674  shft2rab  20833  sca2rab  20837  mbfinf  20985  i1f1lem  21009  i1fres  21025  itg1climres  21034  mbfi1fseqlem4  21038  iblpos  21112  itgposval  21115  cnplimc  21204  ply1remlem  21519  plyremlem  21655  dvdsflsumcom  22413  fsumvma2  22438  vmasum  22440  logfac2  22441  chpchtsum  22443  logfaclbnd  22446  lgsquadlem1  22578  lgsquadlem2  22579  lgsquadlem3  22580  dchrisum0lem1  22650  colinearalg  22979  nbgrael  23160  nbgraeledg  23164  nbgraf1olem1  23173  eupath2lem2  23422  eupath2  23424  pjpreeq  24624  elnlfn  25155  feqmptdf  25802  fmptcof2  25803  dfcnv2  25818  2ndpreima  25826  f1od2  25848  fpwrelmap  25858  iocinioc2  25892  nndiffz1  25898  indpi1  26332  1stmbfm  26529  2ndmbfm  26530  eulerpartlemgh  26609  predfz  27511  elfuns  27793  areacirclem5  28332  fneval  28403  prter3  28872  rmydioph  29208  pw2f1ocnv  29231  funbrafv2b  29911  dfafn5a  29912  2spot2iun2spont  30256  frgraeu  30493  usgreg2spot  30506  bnj1171  31693  islshpat  32235  lfl1dim  32339  glbconxN  32595  cdlemefrs29bpre0  33613  dib1dim  34383  dib1dim2  34386  diclspsn  34412  dihopelvalcpre  34466  dih1dimatlem  34547  mapdordlem1a  34852  hdmapoc  35152