Theorem pm4.71rd 617

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

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359

This theorem is referenced by:  2reu5  3102  ralss  3369  rexss  3370  reuhypd  4709  dfco2a  5329  feu  5578  funbrfv2b  5730  dffn5  5731  eqfnfv2  5787  dff4  5842  fmptco  5860  dff13  5963  exopxfr2  6370  mpt2xopovel  6430  brtpos  6447  dftpos3  6456  opiota  6494  erinxp  6937  qliftfun  6948  pw2f1olem  7171  infm3  9923  prime  10306  hashf1lem2  11660  smueqlem  12957  vdwmc2  13302  acsfiel  13834  subsubc  14005  ismgmid  14665  eqger  14945  eqgid  14947  gaorber  15040  psrbaglefi  16392  znleval  16790  bastop2  17014  elcls2  17093  maxlp  17165  restopn2  17195  restdis  17196  1stccn  17479  tx1cn  17594  tx2cn  17595  imasnopn  17675  imasncld  17676  imasncls  17677  idqtop  17691  tgqtop  17697  filuni  17870  uffix2  17909  cnflf  17987  isfcls  17994  fclsopn  17999  cnfcf  18027  ptcmplem2  18037  xmeter  18416  imasf1oxms  18472  prdsbl  18474  caucfil  19189  cfilucfil4OLD  19226  cfilucfil4  19227  shft2rab  19357  sca2rab  19361  mbfinf  19510  i1f1lem  19534  i1fres  19550  itg1climres  19559  mbfi1fseqlem4  19563  iblpos  19637  itgposval  19640  cnplimc  19727  ply1remlem  20038  plyremlem  20174  dvdsflsumcom  20926  fsumvma2  20951  vmasum  20953  logfac2  20954  chpchtsum  20956  logfaclbnd  20959  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  dchrisum0lem1  21163  nbgrael  21391  nbgraeledg  21395  nbgraf1olem1  21404  eupath2lem2  21653  eupath2  21655  pjpreeq  22853  elnlfn  23384  feqmptdf  24028  fmptcof2  24029  2ndpreima  24049  iocinioc2  24095  indpi1  24372  1stmbfm  24563  2ndmbfm  24564  predfz  25417  colinearalg  25753  areacirclem6  26186  fneval  26257  prter3  26621  rmydioph  26975  pw2f1ocnv  26998  funbrafv2b  27890  dfafn5a  27891  2spot2iun2spont  28088  frgraeu  28157  usgreg2spot  28170  bnj1171  29075  islshpat  29500  lfl1dim  29604  glbconxN  29860  cdlemefrs29bpre0  30878  dib1dim  31648  dib1dim2  31651  diclspsn  31677  dihopelvalcpre  31731  dih1dimatlem  31812  mapdordlem1a  32117  hdmapoc  32417

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361