Theorem pm4.71rd 641

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

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  2reu5  3248  ralss  3495  rexss  3496  reuhypd  4627  exopxfr2  4979  dfco2a  5335  feu  5759  funbrfv2b  5909  dffn5  5910  eqfnfv2  5977  dff4  6036  fmptco  6056  dff13  6159  opiota  6852  mpt2xopovel  6966  brtpos  6982  dftpos3  6991  erinxp  7437  qliftfun  7448  pw2f1olem  7676  infm3  10568  prime  11016  predfz  11914  hashf1lem2  12619  smueqlem  14464  vdwmc2  14929  acsfiel  15560  subsubc  15758  ismgmid  16507  eqger  16867  eqgid  16869  gaorber  16962  symgfix2  17057  psrbaglefi  18596  znleval  19125  bastop2  20010  elcls2  20090  maxlp  20163  restopn2  20193  restdis  20194  1stccn  20478  tx1cn  20624  tx2cn  20625  imasnopn  20705  imasncld  20706  imasncls  20707  idqtop  20721  tgqtop  20727  filuni  20900  uffix2  20939  cnflf  21017  isfcls  21024  fclsopn  21029  cnfcf  21057  ptcmplem2  21068  xmeter  21448  imasf1oxms  21504  prdsbl  21506  caucfil  22253  cfilucfil4  22289  shft2rab  22461  sca2rab  22465  mbfinf  22621  mbfinfOLD  22622  i1f1lem  22647  i1fres  22663  itg1climres  22672  mbfi1fseqlem4  22676  iblpos  22750  itgposval  22753  cnplimc  22842  ply1remlem  23113  plyremlem  23257  dvdsflsumcom  24117  fsumvma2  24142  vmasum  24144  logfac2  24145  chpchtsum  24147  logfaclbnd  24150  lgsquadlem1  24282  lgsquadlem2  24283  lgsquadlem3  24284  dchrisum0lem1  24354  colinearalg  24940  nbgrael  25154  nbgraeledg  25158  nbgraf1olem1  25169  2spot2iun2spont  25619  eupath2lem2  25706  eupath2  25708  frgraeu  25782  usgreg2spot  25795  pjpreeq  27051  elnlfn  27581  fimarab  28244  feqmptdf  28258  fmptcof2  28259  dfcnv2  28279  2ndpreima  28288  f1od2  28309  fpwrelmap  28318  iocinioc2  28361  nndiffz1  28366  indpi1  28843  1stmbfm  29082  2ndmbfm  29083  eulerpartlemgh  29211  bnj1171  29809  mrsubrn  30151  elfuns  30682  fneval  31008  topdifinfindis  31749  phpreu  31929  poimirlem23  31963  poimirlem26  31966  poimirlem27  31967  areacirclem5  32036  prter3  32454  islshpat  32583  lfl1dim  32687  glbconxN  32943  cdlemefrs29bpre0  33963  dib1dim  34733  dib1dim2  34736  diclspsn  34762  dihopelvalcpre  34816  dih1dimatlem  34897  mapdordlem1a  35202  hdmapoc  35502  rmydioph  35869  pw2f1ocnv  35892  funbrafv2b  38661  dfafn5a  38662  nbgrel  39410  nbusgreledg  39421  nbusgredgeu0  39442  umgr2v2enb1  39563