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 666
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 662 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜒𝜓)))
31, 2sylib 208 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  2reu5  3403  ralss  3653  rexss  3654  reuhypd  4865  exopxfr2  5236  dfco2a  5604  feu  6047  funbrfv2b  6207  dffn5  6208  feqmptdf  6218  eqfnfv2  6278  dff4  6339  fmptco  6362  dff13  6477  opiota  7189  mpt2xopovel  7306  brtpos  7321  dftpos3  7330  erinxp  7781  qliftfun  7792  pw2f1olem  8024  infm3  10942  prime  11418  predfz  12421  hashf1lem2  13194  hashle2prv  13214  oddnn02np1  15015  oddge22np1  15016  evennn02n  15017  evennn2n  15018  smueqlem  15155  vdwmc2  15626  acsfiel  16255  subsubc  16453  ismgmid  17204  eqger  17584  eqgid  17586  gaorber  17681  symgfix2  17776  psrbaglefi  19312  znleval  19843  bastop2  20738  elcls2  20818  maxlp  20891  restopn2  20921  restdis  20922  1stccn  21206  tx1cn  21352  tx2cn  21353  imasnopn  21433  imasncld  21434  imasncls  21435  idqtop  21449  tgqtop  21455  filuni  21629  uffix2  21668  cnflf  21746  isfcls  21753  fclsopn  21758  cnfcf  21786  ptcmplem2  21797  xmeter  22178  imasf1oxms  22234  prdsbl  22236  caucfil  23021  cfilucfil4  23058  shft2rab  23216  sca2rab  23220  mbfinf  23372  i1f1lem  23396  i1fres  23412  itg1climres  23421  mbfi1fseqlem4  23425  iblpos  23499  itgposval  23502  cnplimc  23591  ply1remlem  23860  plyremlem  23997  dvdsflsumcom  24848  fsumvma2  24873  vmasum  24875  logfac2  24876  chpchtsum  24878  logfaclbnd  24881  lgsquadlem1  25039  lgsquadlem2  25040  lgsquadlem3  25041  dchrisum0lem1  25139  colinearalg  25724  nbgrel  26159  nbusgreledg  26170  nbusgredgeu0  26191  umgr2v2enb1  26342  iswwlksnx  26634  wspniunwspnon  26722  eupth2lem2  26979  eupth2lems  26998  frgreu  27083  fusgreg2wsp  27092  pjpreeq  28145  elnlfn  28675  fimarab  29328  fmptcof2  29340  dfcnv2  29360  2ndpreima  29369  f1od2  29383  fpwrelmap  29392  iocinioc2  29426  nndiffz1  29431  indpi1  29907  1stmbfm  30145  2ndmbfm  30146  eulerpartlemgh  30263  bnj1171  30829  mrsubrn  31171  elfuns  31717  fneval  32042  topdifinfindis  32865  uncf  33059  phpreu  33064  poimirlem23  33103  poimirlem26  33106  poimirlem27  33107  areacirclem5  33175  prter3  33686  islshpat  33823  lfl1dim  33927  glbconxN  34183  cdlemefrs29bpre0  35203  dib1dim  35973  dib1dim2  35976  diclspsn  36002  dihopelvalcpre  36056  dih1dimatlem  36137  mapdordlem1a  36442  hdmapoc  36742  rmydioph  37100  pw2f1ocnv  37123  rfovcnvf1od  37819  ntrneineine0lem  37902  funbrafv2b  40573  dfafn5a  40574
  Copyright terms: Public domain W3C validator