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  3308  ralss  3562  rexss  3563  reuhypd  4683  exopxfr2  5157  dfco2a  5513  feu  5767  funbrfv2b  5917  dffn5  5918  eqfnfv2  5983  dff4  6046  fmptco  6065  dff13  6167  opiota  6858  mpt2xopovel  6966  brtpos  6982  dftpos3  6991  erinxp  7403  qliftfun  7414  pw2f1olem  7640  infm3  10522  prime  10964  hashf1lem2  12509  smueqlem  14152  vdwmc2  14509  acsfiel  15071  subsubc  15269  ismgmid  16018  eqger  16378  eqgid  16380  gaorber  16473  symgfix2  16568  psrbaglefi  18150  psrbaglefiOLD  18151  znleval  18720  bastop2  19623  elcls2  19702  maxlp  19775  restopn2  19805  restdis  19806  1stccn  20090  tx1cn  20236  tx2cn  20237  imasnopn  20317  imasncld  20318  imasncls  20319  idqtop  20333  tgqtop  20339  filuni  20512  uffix2  20551  cnflf  20629  isfcls  20636  fclsopn  20641  cnfcf  20669  ptcmplem2  20679  xmeter  21062  imasf1oxms  21118  prdsbl  21120  caucfil  21848  cfilucfil4OLD  21885  cfilucfil4  21886  shft2rab  22045  sca2rab  22049  mbfinf  22198  i1f1lem  22222  i1fres  22238  itg1climres  22247  mbfi1fseqlem4  22251  iblpos  22325  itgposval  22328  cnplimc  22417  ply1remlem  22689  plyremlem  22826  dvdsflsumcom  23590  fsumvma2  23615  vmasum  23617  logfac2  23618  chpchtsum  23620  logfaclbnd  23623  lgsquadlem1  23755  lgsquadlem2  23756  lgsquadlem3  23757  dchrisum0lem1  23827  colinearalg  24340  nbgrael  24553  nbgraeledg  24557  nbgraf1olem1  24568  2spot2iun2spont  25018  eupath2lem2  25105  eupath2  25107  frgraeu  25181  usgreg2spot  25194  pjpreeq  26443  elnlfn  26974  fimarab  27631  feqmptdf  27650  fmptcof2  27651  dfcnv2  27672  2ndpreima  27681  f1od2  27704  fpwrelmap  27713  iocinioc2  27750  nndiffz1  27756  indpi1  28196  1stmbfm  28404  2ndmbfm  28405  eulerpartlemgh  28514  mrsubrn  29070  predfz  29500  elfuns  29770  areacirclem5  30316  fneval  30375  prter3  30828  rmydioph  31160  pw2f1ocnv  31183  funbrafv2b  32447  dfafn5a  32448  bnj1171  34199  islshpat  34885  lfl1dim  34989  glbconxN  35245  cdlemefrs29bpre0  36265  dib1dim  37035  dib1dim2  37038  diclspsn  37064  dihopelvalcpre  37118  dih1dimatlem  37199  mapdordlem1a  37504  hdmapoc  37804