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 563
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 562 . 2 (𝜑 → (𝜓 ↔ (𝜓𝜒)))
32biancomd 464 1 (𝜑 → (𝜓 ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  reueubd  3434  2reu5  3746  ralss  4034  rexss  4035  reuhypd  5310  exopxfr2  5708  dfco2a  6092  feu  6547  fcnvres  6549  funbrfv2b  6716  dffn5  6717  feqmptdf  6728  eqfnfv2  6795  dff4  6859  fmptco  6883  dff13  7004  opiota  7746  mpoxopovel  7875  brtpos  7890  dftpos3  7899  erinxp  8360  qliftfun  8371  pw2f1olem  8609  infm3  11588  prime  12051  predfz  13020  hashf1lem2  13802  hashle2prv  13824  oddnn02np1  15685  oddge22np1  15686  evennn02n  15687  evennn2n  15688  smueqlem  15827  vdwmc2  16303  acsfiel  16913  subsubc  17111  ismgmid  17863  eqger  18268  eqgid  18270  gaorber  18376  symgfix2  18473  psrbaglefi  20080  znleval  20629  bastop2  21530  elcls2  21610  maxlp  21683  restopn2  21713  restdis  21714  1stccn  21999  tx1cn  22145  tx2cn  22146  imasnopn  22226  imasncld  22227  imasncls  22228  idqtop  22242  tgqtop  22248  filuni  22421  uffix2  22460  cnflf  22538  isfcls  22545  fclsopn  22550  cnfcf  22578  ptcmplem2  22589  xmeter  22970  imasf1oxms  23026  prdsbl  23028  caucfil  23813  cfilucfil4  23851  shft2rab  24036  sca2rab  24040  mbfinf  24193  i1f1lem  24217  i1fres  24233  itg1climres  24242  mbfi1fseqlem4  24246  iblpos  24320  itgposval  24323  cnplimc  24412  ply1remlem  24683  plyremlem  24820  dvdsflsumcom  25692  fsumvma2  25717  vmasum  25719  logfac2  25720  chpchtsum  25722  logfaclbnd  25725  lgsquadlem1  25883  lgsquadlem2  25884  lgsquadlem3  25885  dchrisum0lem1  26019  colinearalg  26623  nbusgreledg  27062  nbusgredgeu0  27077  umgr2v2enb1  27235  iswwlksnx  27545  wspniunwspnon  27629  clwlknf1oclwwlknlem2  27788  clwlknf1oclwwlkn  27790  eupth2lem2  27925  eupth2lems  27944  frgrncvvdeqlem2  28006  fusgr2wsp2nb  28040  fusgreg2wsp  28042  pjpreeq  29102  elnlfn  29632  nfpconfp  30305  fimarab  30318  fmptcof2  30330  dfcnv2  30350  2ndpreima  30369  f1od2  30383  fpwrelmap  30395  iocinioc2  30428  nndiffz1  30435  indpi1  31178  1stmbfm  31417  2ndmbfm  31418  eulerpartlemgh  31535  bnj1171  32169  mrsubrn  32657  elfuns  33273  fneval  33597  bj-imdirval3  34366  topdifinfindis  34509  uncf  34752  phpreu  34757  poimirlem23  34796  poimirlem26  34799  poimirlem27  34800  areacirclem5  34867  erim2  35791  prter3  35898  islshpat  36033  lfl1dim  36137  glbconxN  36394  cdlemefrs29bpre0  37412  dib1dim  38181  dib1dim2  38184  diclspsn  38210  dihopelvalcpre  38264  dih1dimatlem  38345  mapdordlem1a  38650  hdmapoc  38947  prjspeclsp  39140  rmydioph  39489  pw2f1ocnv  39512  rfovcnvf1od  40228  ntrneineine0lem  40311  funbrafv2b  43235  dfafn5a  43236  prprelb  43555
  Copyright terms: Public domain W3C validator