MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71rd Unicode version

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
StepHypRef Expression
1 pm4.71rd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 pm4.71r 613 . 2  |-  ( ( ps  ->  ch )  <->  ( ps  <->  ( ch  /\  ps ) ) )
31, 2sylib 189 1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  2reu5  3106  ralss  3373  rexss  3374  reuhypd  4713  dfco2a  5333  feu  5582  funbrfv2b  5734  dffn5  5735  eqfnfv2  5791  dff4  5846  fmptco  5864  dff13  5967  exopxfr2  6374  mpt2xopovel  6434  brtpos  6451  dftpos3  6460  opiota  6498  erinxp  6941  qliftfun  6952  pw2f1olem  7175  infm3  9927  prime  10310  hashf1lem2  11664  smueqlem  12961  vdwmc2  13306  acsfiel  13838  subsubc  14009  ismgmid  14669  eqger  14949  eqgid  14951  gaorber  15044  psrbaglefi  16396  znleval  16794  bastop2  17018  elcls2  17097  maxlp  17169  restopn2  17199  restdis  17200  1stccn  17483  tx1cn  17598  tx2cn  17599  imasnopn  17679  imasncld  17680  imasncls  17681  idqtop  17695  tgqtop  17701  filuni  17874  uffix2  17913  cnflf  17991  isfcls  17998  fclsopn  18003  cnfcf  18031  ptcmplem2  18041  xmeter  18420  imasf1oxms  18476  prdsbl  18478  caucfil  19193  cfilucfil4OLD  19230  cfilucfil4  19231  shft2rab  19361  sca2rab  19365  mbfinf  19514  i1f1lem  19538  i1fres  19554  itg1climres  19563  mbfi1fseqlem4  19567  iblpos  19641  itgposval  19644  cnplimc  19731  ply1remlem  20042  plyremlem  20178  dvdsflsumcom  20930  fsumvma2  20955  vmasum  20957  logfac2  20958  chpchtsum  20960  logfaclbnd  20963  lgsquadlem1  21095  lgsquadlem2  21096  lgsquadlem3  21097  dchrisum0lem1  21167  nbgrael  21395  nbgraeledg  21399  nbgraf1olem1  21408  eupath2lem2  21657  eupath2  21659  pjpreeq  22857  elnlfn  23388  feqmptdf  24032  fmptcof2  24033  2ndpreima  24053  iocinioc2  24099  indpi1  24376  1stmbfm  24567  2ndmbfm  24568  predfz  25421  colinearalg  25757  areacirclem6  26190  fneval  26261  prter3  26625  rmydioph  26979  pw2f1ocnv  27002  funbrafv2b  27894  dfafn5a  27895  2spot2iun2spont  28092  frgraeu  28161  usgreg2spot  28174  bnj1171  29079  islshpat  29504  lfl1dim  29608  glbconxN  29864  cdlemefrs29bpre0  30882  dib1dim  31652  dib1dim2  31655  diclspsn  31681  dihopelvalcpre  31735  dih1dimatlem  31816  mapdordlem1a  32121  hdmapoc  32421
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
  Copyright terms: Public domain W3C validator