Theorem pm4.71rd 635

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 631	. 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  3312  ralss  3566  rexss  3567  reuhypd  4674  exopxfr2  5145  dfco2a  5505  feu  5759  funbrfv2b  5910  dffn5  5911  eqfnfv2  5974  dff4  6033  fmptco  6052  dff13  6152  opiota  6840  mpt2xopovel  6945  brtpos  6961  dftpos3  6970  erinxp  7382  qliftfun  7393  pw2f1olem  7618  infm3  10498  prime  10937  hashf1lem2  12467  smueqlem  13995  vdwmc2  14352  acsfiel  14905  subsubc  15076  ismgmid  15748  eqger  16046  eqgid  16048  gaorber  16141  symgfix2  16236  psrbaglefi  17794  psrbaglefiOLD  17795  znleval  18360  bastop2  19262  elcls2  19341  maxlp  19414  restopn2  19444  restdis  19445  1stccn  19730  tx1cn  19845  tx2cn  19846  imasnopn  19926  imasncld  19927  imasncls  19928  idqtop  19942  tgqtop  19948  filuni  20121  uffix2  20160  cnflf  20238  isfcls  20245  fclsopn  20250  cnfcf  20278  ptcmplem2  20288  xmeter  20671  imasf1oxms  20727  prdsbl  20729  caucfil  21457  cfilucfil4OLD  21494  cfilucfil4  21495  shft2rab  21654  sca2rab  21658  mbfinf  21807  i1f1lem  21831  i1fres  21847  itg1climres  21856  mbfi1fseqlem4  21860  iblpos  21934  itgposval  21937  cnplimc  22026  ply1remlem  22298  plyremlem  22434  dvdsflsumcom  23192  fsumvma2  23217  vmasum  23219  logfac2  23220  chpchtsum  23222  logfaclbnd  23225  lgsquadlem1  23357  lgsquadlem2  23358  lgsquadlem3  23359  dchrisum0lem1  23429  colinearalg  23889  nbgrael  24102  nbgraeledg  24106  nbgraf1olem1  24117  2spot2iun2spont  24567  eupath2lem2  24654  eupath2  24656  frgraeu  24731  usgreg2spot  24744  pjpreeq  25992  elnlfn  26523  feqmptdf  27173  fmptcof2  27174  dfcnv2  27189  2ndpreima  27197  f1od2  27219  fpwrelmap  27228  iocinioc2  27258  nndiffz1  27264  indpi1  27675  1stmbfm  27871  2ndmbfm  27872  eulerpartlemgh  27957  predfz  28860  elfuns  29142  areacirclem5  29688  fneval  29759  prter3  30227  rmydioph  30560  pw2f1ocnv  30583  funbrafv2b  31711  dfafn5a  31712  bnj1171  33135  islshpat  33814  lfl1dim  33918  glbconxN  34174  cdlemefrs29bpre0  35192  dib1dim  35962  dib1dim2  35965  diclspsn  35991  dihopelvalcpre  36045  dih1dimatlem  36126  mapdordlem1a  36431  hdmapoc  36731