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 664
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 660 . 2 ((𝜓𝜒) ↔ (𝜓 ↔ (𝜒𝜓)))
31, 2sylib 206 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  2reu5  3379  ralss  3627  rexss  3628  reuhypd  4813  exopxfr2  5173  dfco2a  5535  feu  5975  funbrfv2b  6132  dffn5  6133  feqmptdf  6143  eqfnfv2  6202  dff4  6263  fmptco  6285  dff13  6391  opiota  7092  mpt2xopovel  7207  brtpos  7222  dftpos3  7231  erinxp  7682  qliftfun  7693  pw2f1olem  7923  infm3  10828  prime  11287  predfz  12285  hashf1lem2  13046  oddnn02np1  14853  oddge22np1  14854  evennn02n  14855  evennn2n  14856  smueqlem  14993  vdwmc2  15464  acsfiel  16081  subsubc  16279  ismgmid  17030  eqger  17410  eqgid  17412  gaorber  17507  symgfix2  17602  psrbaglefi  19136  znleval  19664  bastop2  20548  elcls2  20627  maxlp  20700  restopn2  20730  restdis  20731  1stccn  21015  tx1cn  21161  tx2cn  21162  imasnopn  21242  imasncld  21243  imasncls  21244  idqtop  21258  tgqtop  21264  filuni  21438  uffix2  21477  cnflf  21555  isfcls  21562  fclsopn  21567  cnfcf  21595  ptcmplem2  21606  xmeter  21986  imasf1oxms  22042  prdsbl  22044  caucfil  22804  cfilucfil4  22840  shft2rab  22997  sca2rab  23001  mbfinf  23152  i1f1lem  23176  i1fres  23192  itg1climres  23201  mbfi1fseqlem4  23205  iblpos  23279  itgposval  23282  cnplimc  23371  ply1remlem  23640  plyremlem  23777  dvdsflsumcom  24628  fsumvma2  24653  vmasum  24655  logfac2  24656  chpchtsum  24658  logfaclbnd  24661  lgsquadlem1  24819  lgsquadlem2  24820  lgsquadlem3  24821  dchrisum0lem1  24919  colinearalg  25505  nbgrael  25718  nbgraeledg  25722  nbgraf1olem1  25733  2spot2iun2spont  26181  eupath2lem2  26268  eupath2  26270  frgraeu  26344  usgreg2spot  26357  pjpreeq  27444  elnlfn  27974  fimarab  28628  fmptcof2  28642  dfcnv2  28662  2ndpreima  28671  f1od2  28690  fpwrelmap  28699  iocinioc2  28734  nndiffz1  28739  indpi1  29214  1stmbfm  29452  2ndmbfm  29453  eulerpartlemgh  29570  bnj1171  30125  mrsubrn  30467  elfuns  30995  fneval  31320  topdifinfindis  32170  uncf  32358  phpreu  32363  poimirlem23  32402  poimirlem26  32405  poimirlem27  32406  areacirclem5  32474  prter3  32985  islshpat  33122  lfl1dim  33226  glbconxN  33482  cdlemefrs29bpre0  34502  dib1dim  35272  dib1dim2  35275  diclspsn  35301  dihopelvalcpre  35355  dih1dimatlem  35436  mapdordlem1a  35741  hdmapoc  36041  rmydioph  36399  pw2f1ocnv  36422  rfovcnvf1od  37118  ntrneineine0lem  37201  funbrafv2b  39690  dfafn5a  39691  nbgrel  40563  nbusgreledg  40574  nbusgredgeu0  40595  umgr2v2enb1  40741  iswwlksnx  41041  wspniunwspnon  41129  eupth2lem2  41386  eupth2lems  41405  frgreu  41490  fusgreg2wsp  41499
  Copyright terms: Public domain W3C validator