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

Theorem pm4.71rd 616
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 612 . 2  |-  ( ( ps  ->  ch )  <->  ( ps  <->  ( ch  /\  ps ) ) )
31, 2sylib 188 1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  2reu5  2973  ralss  3239  rexss  3240  reuhypd  4561  dfco2a  5173  feu  5417  funbrfv2b  5567  dffn5  5568  eqfnfv2  5623  dff4  5674  fmptco  5691  dff13  5783  exopxfr2  6184  brtpos  6243  dftpos3  6252  opiota  6290  erinxp  6733  qliftfun  6743  pw2f1olem  6966  infm3  9713  prime  10092  hashf1lem2  11394  smueqlem  12681  vdwmc2  13026  acsfiel  13556  subsubc  13727  ismgmid  14387  eqger  14667  eqgid  14669  gaorber  14762  psrbaglefi  16118  znleval  16508  bastop2  16732  elcls2  16811  maxlp  16878  restopn2  16908  restdis  16909  1stccn  17189  tx1cn  17303  tx2cn  17304  idqtop  17397  tgqtop  17403  filuni  17580  uffix2  17619  cnflf  17697  isfcls  17704  fclsopn  17709  cnfcf  17737  ptcmplem2  17747  xmeter  17979  imasf1oxms  18035  prdsbl  18037  caucfil  18709  shft2rab  18867  sca2rab  18871  mbfinf  19020  i1f1lem  19044  i1fres  19060  itg1climres  19069  mbfi1fseqlem4  19073  iblpos  19147  itgposval  19150  cnplimc  19237  ply1remlem  19548  plyremlem  19684  dvdsflsumcom  20428  fsumvma2  20453  vmasum  20455  logfac2  20456  chpchtsum  20458  logfaclbnd  20461  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  dchrisum0lem1  20665  pjpreeq  21977  elnlfn  22508  xppreima  23211  feqmptdf  23228  fmptcof2  23229  iocinioc2  23272  1stmbfm  23565  2ndmbfm  23566  indpi1  23605  eupath2lem2  23902  eupath2  23904  predfz  24203  colinearalg  24538  areacirclem6  24930  dfoprab4pop  25037  fneval  26287  prter3  26750  rmydioph  27107  pw2f1ocnv  27130  funbrafv2b  28021  dfafn5a  28022  mpt2xopovel  28086  nbgrael  28141  nbgraeledg  28145  bnj1171  29030  islshpat  29207  lfl1dim  29311  glbconxN  29567  cdlemefrs29bpre0  30585  dib1dim  31355  dib1dim2  31358  diclspsn  31384  dihopelvalcpre  31438  dih1dimatlem  31519  mapdordlem1a  31824  hdmapoc  32124
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 177  df-an 360
  Copyright terms: Public domain W3C validator