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

Theorem pm4.71rd 665
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 661 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜒𝜓)))
31, 2sylib 207 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  2reu5  3383  ralss  3631  rexss  3632  reuhypd  4821  exopxfr2  5188  dfco2a  5552  feu  5993  funbrfv2b  6150  dffn5  6151  feqmptdf  6161  eqfnfv2  6220  dff4  6281  fmptco  6303  dff13  6416  opiota  7118  mpt2xopovel  7233  brtpos  7248  dftpos3  7257  erinxp  7708  qliftfun  7719  pw2f1olem  7949  infm3  10861  prime  11334  predfz  12333  hashf1lem2  13097  oddnn02np1  14910  oddge22np1  14911  evennn02n  14912  evennn2n  14913  smueqlem  15050  vdwmc2  15521  acsfiel  16138  subsubc  16336  ismgmid  17087  eqger  17467  eqgid  17469  gaorber  17564  symgfix2  17659  psrbaglefi  19193  znleval  19722  bastop2  20609  elcls2  20688  maxlp  20761  restopn2  20791  restdis  20792  1stccn  21076  tx1cn  21222  tx2cn  21223  imasnopn  21303  imasncld  21304  imasncls  21305  idqtop  21319  tgqtop  21325  filuni  21499  uffix2  21538  cnflf  21616  isfcls  21623  fclsopn  21628  cnfcf  21656  ptcmplem2  21667  xmeter  22048  imasf1oxms  22104  prdsbl  22106  caucfil  22889  cfilucfil4  22926  shft2rab  23083  sca2rab  23087  mbfinf  23238  i1f1lem  23262  i1fres  23278  itg1climres  23287  mbfi1fseqlem4  23291  iblpos  23365  itgposval  23368  cnplimc  23457  ply1remlem  23726  plyremlem  23863  dvdsflsumcom  24714  fsumvma2  24739  vmasum  24741  logfac2  24742  chpchtsum  24744  logfaclbnd  24747  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  dchrisum0lem1  25005  colinearalg  25590  nbgrael  25955  nbgraeledg  25959  nbgraf1olem1  25970  2spot2iun2spont  26418  eupath2lem2  26505  eupath2  26507  frgraeu  26581  usgreg2spot  26594  pjpreeq  27641  elnlfn  28171  fimarab  28825  fmptcof2  28839  dfcnv2  28859  2ndpreima  28868  f1od2  28887  fpwrelmap  28896  iocinioc2  28931  nndiffz1  28936  indpi1  29411  1stmbfm  29649  2ndmbfm  29650  eulerpartlemgh  29767  bnj1171  30322  mrsubrn  30664  elfuns  31192  fneval  31517  topdifinfindis  32370  uncf  32558  phpreu  32563  poimirlem23  32602  poimirlem26  32605  poimirlem27  32606  areacirclem5  32674  prter3  33185  islshpat  33322  lfl1dim  33426  glbconxN  33682  cdlemefrs29bpre0  34702  dib1dim  35472  dib1dim2  35475  diclspsn  35501  dihopelvalcpre  35555  dih1dimatlem  35636  mapdordlem1a  35941  hdmapoc  36241  rmydioph  36599  pw2f1ocnv  36622  rfovcnvf1od  37318  ntrneineine0lem  37401  funbrafv2b  39888  dfafn5a  39889  nbgrel  40564  nbusgreledg  40575  nbusgredgeu0  40596  umgr2v2enb1  40742  iswwlksnx  41042  wspniunwspnon  41130  eupth2lem2  41387  eupth2lems  41406  frgreu  41491  fusgreg2wsp  41500
  Copyright terms: Public domain W3C validator