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  3078  ralss  3345  rexss  3346  reuhypd  4683  dfco2a  5303  feu  5552  funbrfv2b  5703  dffn5  5704  eqfnfv2  5760  dff4  5815  fmptco  5833  dff13  5936  exopxfr2  6343  mpt2xopovel  6400  brtpos  6417  dftpos3  6426  opiota  6464  erinxp  6907  qliftfun  6918  pw2f1olem  7141  infm3  9892  prime  10275  hashf1lem2  11625  smueqlem  12922  vdwmc2  13267  acsfiel  13799  subsubc  13970  ismgmid  14630  eqger  14910  eqgid  14912  gaorber  15005  psrbaglefi  16357  znleval  16751  bastop2  16975  elcls2  17054  maxlp  17126  restopn2  17156  restdis  17157  1stccn  17440  tx1cn  17555  tx2cn  17556  imasnopn  17636  imasncld  17637  imasncls  17638  idqtop  17652  tgqtop  17658  filuni  17831  uffix2  17870  cnflf  17948  isfcls  17955  fclsopn  17960  cnfcf  17988  ptcmplem2  17998  xmeter  18346  imasf1oxms  18402  prdsbl  18404  caucfil  19100  cfilucfil4  19136  shft2rab  19264  sca2rab  19268  mbfinf  19417  i1f1lem  19441  i1fres  19457  itg1climres  19466  mbfi1fseqlem4  19470  iblpos  19544  itgposval  19547  cnplimc  19634  ply1remlem  19945  plyremlem  20081  dvdsflsumcom  20833  fsumvma2  20858  vmasum  20860  logfac2  20861  chpchtsum  20863  logfaclbnd  20866  lgsquadlem1  20998  lgsquadlem2  20999  lgsquadlem3  21000  dchrisum0lem1  21070  nbgrael  21297  nbgraeledg  21301  nbgraf1olem1  21310  eupath2lem2  21541  eupath2  21543  pjpreeq  22741  elnlfn  23272  feqmptdf  23910  fmptcof2  23911  2ndpreima  23930  iocinioc2  23971  indpi1  24208  1stmbfm  24397  2ndmbfm  24398  predfz  25220  colinearalg  25556  areacirclem6  25980  fneval  26051  prter3  26415  rmydioph  26769  pw2f1ocnv  26792  funbrafv2b  27685  dfafn5a  27686  bnj1171  28700  islshpat  29183  lfl1dim  29287  glbconxN  29543  cdlemefrs29bpre0  30561  dib1dim  31331  dib1dim2  31334  diclspsn  31360  dihopelvalcpre  31414  dih1dimatlem  31495  mapdordlem1a  31800  hdmapoc  32100
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