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  3170  ralss  3421  rexss  3422  reuhypd  4522  exopxfr2  4987  dfco2a  5341  feu  5590  funbrfv2b  5739  dffn5  5740  eqfnfv2  5801  dff4  5860  fmptco  5879  dff13  5974  opiota  6636  mpt2xopovel  6740  brtpos  6757  dftpos3  6766  erinxp  7177  qliftfun  7188  pw2f1olem  7418  infm3  10292  prime  10725  hashf1lem2  12212  smueqlem  13689  vdwmc2  14043  acsfiel  14595  subsubc  14766  ismgmid  15438  eqger  15734  eqgid  15736  gaorber  15829  symgfix2  15924  psrbaglefi  17444  psrbaglefiOLD  17445  znleval  17990  bastop2  18602  elcls2  18681  maxlp  18754  restopn2  18784  restdis  18785  1stccn  19070  tx1cn  19185  tx2cn  19186  imasnopn  19266  imasncld  19267  imasncls  19268  idqtop  19282  tgqtop  19288  filuni  19461  uffix2  19500  cnflf  19578  isfcls  19585  fclsopn  19590  cnfcf  19618  ptcmplem2  19628  xmeter  20011  imasf1oxms  20067  prdsbl  20069  caucfil  20797  cfilucfil4OLD  20834  cfilucfil4  20835  shft2rab  20994  sca2rab  20998  mbfinf  21146  i1f1lem  21170  i1fres  21186  itg1climres  21195  mbfi1fseqlem4  21199  iblpos  21273  itgposval  21276  cnplimc  21365  ply1remlem  21637  plyremlem  21773  dvdsflsumcom  22531  fsumvma2  22556  vmasum  22558  logfac2  22559  chpchtsum  22561  logfaclbnd  22564  lgsquadlem1  22696  lgsquadlem2  22697  lgsquadlem3  22698  dchrisum0lem1  22768  colinearalg  23159  nbgrael  23340  nbgraeledg  23344  nbgraf1olem1  23353  eupath2lem2  23602  eupath2  23604  pjpreeq  24804  elnlfn  25335  feqmptdf  25981  fmptcof2  25982  dfcnv2  25997  2ndpreima  26005  f1od2  26027  fpwrelmap  26036  iocinioc2  26072  nndiffz1  26078  indpi1  26481  1stmbfm  26678  2ndmbfm  26679  eulerpartlemgh  26764  predfz  27667  elfuns  27949  areacirclem5  28491  fneval  28562  prter3  29030  rmydioph  29366  pw2f1ocnv  29389  funbrafv2b  30068  dfafn5a  30069  2spot2iun2spont  30413  frgraeu  30650  usgreg2spot  30663  bnj1171  31994  islshpat  32665  lfl1dim  32769  glbconxN  33025  cdlemefrs29bpre0  34043  dib1dim  34813  dib1dim2  34816  diclspsn  34842  dihopelvalcpre  34896  dih1dimatlem  34977  mapdordlem1a  35282  hdmapoc  35582