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

Theorem pm4.71rd 566
 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 . . 3 (𝜑 → (𝜓𝜒))
21pm4.71d 565 . 2 (𝜑 → (𝜓 ↔ (𝜓𝜒)))
32biancomd 467 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  reueubd  3409  2reu5  3724  ralss  4012  rexss  4013  reuhypd  5297  exopxfr2  5692  dfco2a  6077  feu  6535  fcnvres  6537  funbrfv2b  6705  dffn5  6706  feqmptdf  6717  eqfnfv2  6785  dff4  6849  fmptco  6873  dff13  6996  opiota  7743  mpoxopovel  7873  brtpos  7888  dftpos3  7897  erinxp  8358  qliftfun  8369  pw2f1olem  8608  infm3  11587  prime  12051  predfz  13027  hashf1lem2  13810  hashle2prv  13832  oddnn02np1  15688  oddge22np1  15689  evennn02n  15690  evennn2n  15691  smueqlem  15828  vdwmc2  16304  acsfiel  16916  subsubc  17114  ismgmid  17866  eqger  18321  eqgid  18323  gaorber  18429  symgfix2  18535  znleval  20244  psrbaglefi  20608  bastop2  21597  elcls2  21677  maxlp  21750  restopn2  21780  restdis  21781  1stccn  22066  tx1cn  22212  tx2cn  22213  imasnopn  22293  imasncld  22294  imasncls  22295  idqtop  22309  tgqtop  22315  filuni  22488  uffix2  22527  cnflf  22605  isfcls  22612  fclsopn  22617  cnfcf  22645  ptcmplem2  22656  xmeter  23038  imasf1oxms  23094  prdsbl  23096  caucfil  23885  cfilucfil4  23923  shft2rab  24110  sca2rab  24114  mbfinf  24267  i1f1lem  24291  i1fres  24307  itg1climres  24316  mbfi1fseqlem4  24320  iblpos  24394  itgposval  24397  cnplimc  24488  ply1remlem  24761  plyremlem  24898  dvdsflsumcom  25771  fsumvma2  25796  vmasum  25798  logfac2  25799  chpchtsum  25801  logfaclbnd  25804  lgsquadlem1  25962  lgsquadlem2  25963  lgsquadlem3  25964  dchrisum0lem1  26098  colinearalg  26702  nbusgreledg  27141  nbusgredgeu0  27156  umgr2v2enb1  27314  iswwlksnx  27624  wspniunwspnon  27707  clwlknf1oclwwlknlem2  27865  clwlknf1oclwwlkn  27867  eupth2lem2  28002  eupth2lems  28021  frgrncvvdeqlem2  28083  fusgr2wsp2nb  28117  fusgreg2wsp  28119  pjpreeq  29179  elnlfn  29709  eqrrabd  30270  nfpconfp  30385  fimarab  30398  fmptcof2  30410  dfcnv2  30430  2ndpreima  30451  f1od2  30467  fpwrelmap  30479  iocinioc2  30512  nndiffz1  30519  indpi1  31353  1stmbfm  31592  2ndmbfm  31593  eulerpartlemgh  31710  bnj1171  32346  mrsubrn  32834  elfuns  33450  fneval  33774  bj-imdirval3  34560  topdifinfindis  34724  uncf  34994  phpreu  34999  poimirlem23  35038  poimirlem26  35041  poimirlem27  35042  areacirclem5  35107  erim2  36029  prter3  36136  islshpat  36271  lfl1dim  36375  glbconxN  36632  cdlemefrs29bpre0  37650  dib1dim  38419  dib1dim2  38422  diclspsn  38448  dihopelvalcpre  38502  dih1dimatlem  38583  mapdordlem1a  38888  hdmapoc  39185  prjspeclsp  39536  rmydioph  39885  pw2f1ocnv  39908  rfovcnvf1od  40636  ntrneineine0lem  40719  funbrafv2b  43654  dfafn5a  43655  prprelb  43972
 Copyright terms: Public domain W3C validator