Theorem pm4.71rd 647

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

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  2reu5  3236  ralss  3481  rexss  3482  reuhypd  4627  exopxfr2  4984  dfco2a  5342  feu  5771  funbrfv2b  5923  dffn5  5924  feqmptdf  5934  eqfnfv2  5992  dff4  6051  fmptco  6072  dff13  6177  opiota  6871  mpt2xopovel  6985  brtpos  7000  dftpos3  7009  erinxp  7455  qliftfun  7466  pw2f1olem  7694  infm3  10590  prime  11039  predfz  11941  hashf1lem2  12660  smueqlem  14543  vdwmc2  15008  acsfiel  15638  subsubc  15836  ismgmid  16585  eqger  16945  eqgid  16947  gaorber  17040  symgfix2  17135  psrbaglefi  18673  znleval  19202  bastop2  20087  elcls2  20167  maxlp  20240  restopn2  20270  restdis  20271  1stccn  20555  tx1cn  20701  tx2cn  20702  imasnopn  20782  imasncld  20783  imasncls  20784  idqtop  20798  tgqtop  20804  filuni  20978  uffix2  21017  cnflf  21095  isfcls  21102  fclsopn  21107  cnfcf  21135  ptcmplem2  21146  xmeter  21526  imasf1oxms  21582  prdsbl  21584  caucfil  22331  cfilucfil4  22367  shft2rab  22539  sca2rab  22543  mbfinf  22700  mbfinfOLD  22701  i1f1lem  22726  i1fres  22742  itg1climres  22751  mbfi1fseqlem4  22755  iblpos  22829  itgposval  22832  cnplimc  22921  ply1remlem  23192  plyremlem  23336  dvdsflsumcom  24196  fsumvma2  24221  vmasum  24223  logfac2  24224  chpchtsum  24226  logfaclbnd  24229  lgsquadlem1  24361  lgsquadlem2  24362  lgsquadlem3  24363  dchrisum0lem1  24433  colinearalg  25019  nbgrael  25233  nbgraeledg  25237  nbgraf1olem1  25248  2spot2iun2spont  25698  eupath2lem2  25785  eupath2  25787  frgraeu  25861  usgreg2spot  25874  pjpreeq  27132  elnlfn  27662  fimarab  28320  fmptcof2  28334  dfcnv2  28354  2ndpreima  28363  f1od2  28384  fpwrelmap  28393  iocinioc2  28436  nndiffz1  28441  indpi1  28917  1stmbfm  29155  2ndmbfm  29156  eulerpartlemgh  29284  bnj1171  29881  mrsubrn  30223  elfuns  30753  fneval  31079  topdifinfindis  31819  phpreu  31993  poimirlem23  32027  poimirlem26  32030  poimirlem27  32031  areacirclem5  32100  prter3  32518  islshpat  32654  lfl1dim  32758  glbconxN  33014  cdlemefrs29bpre0  34034  dib1dim  34804  dib1dim2  34807  diclspsn  34833  dihopelvalcpre  34887  dih1dimatlem  34968  mapdordlem1a  35273  hdmapoc  35573  rmydioph  35940  pw2f1ocnv  35963  funbrafv2b  38806  dfafn5a  38807  nbgrel  39574  nbusgreledg  39585  nbusgredgeu0  39606  umgr2v2enb1  39749  eupth2lem2  40131  eupth2lems  40150