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 668
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 664 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜒𝜓)))
31, 2sylib 208 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 385
This theorem is referenced by:  reueubd  3194  2reu5  3449  ralss  3701  rexss  3702  reuhypd  4925  exopxfr2  5299  dfco2a  5673  feu  6118  funbrfv2b  6279  dffn5  6280  feqmptdf  6290  eqfnfv2  6352  dff4  6413  fmptco  6436  dff13  6552  opiota  7273  mpt2xopovel  7391  brtpos  7406  dftpos3  7415  erinxp  7864  qliftfun  7875  pw2f1olem  8105  infm3  11020  prime  11496  predfz  12503  hashf1lem2  13278  hashle2prv  13298  oddnn02np1  15119  oddge22np1  15120  evennn02n  15121  evennn2n  15122  smueqlem  15259  vdwmc2  15730  acsfiel  16362  subsubc  16560  ismgmid  17311  eqger  17691  eqgid  17693  gaorber  17787  symgfix2  17882  psrbaglefi  19420  znleval  19951  bastop2  20846  elcls2  20926  maxlp  20999  restopn2  21029  restdis  21030  1stccn  21314  tx1cn  21460  tx2cn  21461  imasnopn  21541  imasncld  21542  imasncls  21543  idqtop  21557  tgqtop  21563  filuni  21736  uffix2  21775  cnflf  21853  isfcls  21860  fclsopn  21865  cnfcf  21893  ptcmplem2  21904  xmeter  22285  imasf1oxms  22341  prdsbl  22343  caucfil  23127  cfilucfil4  23164  shft2rab  23322  sca2rab  23326  mbfinf  23477  i1f1lem  23501  i1fres  23517  itg1climres  23526  mbfi1fseqlem4  23530  iblpos  23604  itgposval  23607  cnplimc  23696  ply1remlem  23967  plyremlem  24104  dvdsflsumcom  24959  fsumvma2  24984  vmasum  24986  logfac2  24987  chpchtsum  24989  logfaclbnd  24992  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  dchrisum0lem1  25250  colinearalg  25835  nbgrelOLD  26279  nbusgreledg  26294  nbusgredgeu0  26314  umgr2v2enb1  26478  iswwlksnx  26788  wspniunwspnon  26888  eupth2lem2  27197  eupth2lems  27216  frgrncvvdeqlem2  27280  fusgr2wsp2nb  27314  fusgreg2wsp  27316  pjpreeq  28385  elnlfn  28915  fimarab  29573  fmptcof2  29585  dfcnv2  29604  2ndpreima  29613  f1od2  29627  fpwrelmap  29636  iocinioc2  29669  nndiffz1  29676  indpi1  30210  1stmbfm  30450  2ndmbfm  30451  eulerpartlemgh  30568  bnj1171  31194  mrsubrn  31536  elfuns  32147  fneval  32472  topdifinfindis  33324  uncf  33518  phpreu  33523  poimirlem23  33562  poimirlem26  33565  poimirlem27  33566  areacirclem5  33634  prter3  34486  islshpat  34622  lfl1dim  34726  glbconxN  34982  cdlemefrs29bpre0  36001  dib1dim  36771  dib1dim2  36774  diclspsn  36800  dihopelvalcpre  36854  dih1dimatlem  36935  mapdordlem1a  37240  hdmapoc  37540  rmydioph  37898  pw2f1ocnv  37921  rfovcnvf1od  38615  ntrneineine0lem  38698  funbrafv2b  41560  dfafn5a  41561
  Copyright terms: Public domain W3C validator