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

Theorem pm4.71rd 635
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
Assertion
Ref Expression
pm4.71rd

Proof of Theorem pm4.71rd
StepHypRef Expression
1 pm4.71rd.1 . 2
2 pm4.71r 631 . 2
31, 2sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  2reu5  3308  ralss  3565  rexss  3566  reuhypd  4679  exopxfr2  5152  dfco2a  5512  feu  5766  funbrfv2b  5917  dffn5  5918  eqfnfv2  5982  dff4  6045  fmptco  6064  dff13  6166  opiota  6859  mpt2xopovel  6967  brtpos  6983  dftpos3  6992  erinxp  7404  qliftfun  7415  pw2f1olem  7641  infm3  10527  prime  10968  hashf1lem2  12505  smueqlem  14140  vdwmc2  14497  acsfiel  15051  subsubc  15222  ismgmid  15891  eqger  16251  eqgid  16253  gaorber  16346  symgfix2  16441  psrbaglefi  18023  psrbaglefiOLD  18024  znleval  18593  bastop2  19496  elcls2  19575  maxlp  19648  restopn2  19678  restdis  19679  1stccn  19964  tx1cn  20110  tx2cn  20111  imasnopn  20191  imasncld  20192  imasncls  20193  idqtop  20207  tgqtop  20213  filuni  20386  uffix2  20425  cnflf  20503  isfcls  20510  fclsopn  20515  cnfcf  20543  ptcmplem2  20553  xmeter  20936  imasf1oxms  20992  prdsbl  20994  caucfil  21722  cfilucfil4OLD  21759  cfilucfil4  21760  shft2rab  21919  sca2rab  21923  mbfinf  22072  i1f1lem  22096  i1fres  22112  itg1climres  22121  mbfi1fseqlem4  22125  iblpos  22199  itgposval  22202  cnplimc  22291  ply1remlem  22563  plyremlem  22700  dvdsflsumcom  23464  fsumvma2  23489  vmasum  23491  logfac2  23492  chpchtsum  23494  logfaclbnd  23497  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  dchrisum0lem1  23701  colinearalg  24213  nbgrael  24426  nbgraeledg  24430  nbgraf1olem1  24441  2spot2iun2spont  24891  eupath2lem2  24978  eupath2  24980  frgraeu  25054  usgreg2spot  25067  pjpreeq  26316  elnlfn  26847  fimarab  27483  feqmptdf  27501  fmptcof2  27502  dfcnv2  27517  2ndpreima  27525  f1od2  27547  fpwrelmap  27556  iocinioc2  27590  nndiffz1  27596  indpi1  28035  1stmbfm  28231  2ndmbfm  28232  eulerpartlemgh  28317  mrsubrn  28873  predfz  29283  elfuns  29565  areacirclem5  30111  fneval  30170  prter3  30623  rmydioph  30956  pw2f1ocnv  30979  funbrafv2b  32244  dfafn5a  32245  bnj1171  34056  islshpat  34742  lfl1dim  34846  glbconxN  35102  cdlemefrs29bpre0  36122  dib1dim  36892  dib1dim2  36895  diclspsn  36921  dihopelvalcpre  36975  dih1dimatlem  37056  mapdordlem1a  37361  hdmapoc  37661
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 185  df-an 371
  Copyright terms: Public domain W3C validator