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

Theorem pm4.71ri 561
Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.)
Hypothesis
Ref Expression
pm4.71ri.1 (𝜑𝜓)
Assertion
Ref Expression
pm4.71ri (𝜑 ↔ (𝜓𝜑))

Proof of Theorem pm4.71ri
StepHypRef Expression
1 pm4.71ri.1 . . 3 (𝜑𝜓)
21pm4.71i 560 . 2 (𝜑 ↔ (𝜑𝜓))
32biancomi 463 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:  anabs7  660  biadaniALT  818  biadan2OLD  820  orabs  994  prlem2  1049  dfeumo  2617  dfeu  2679  2moswapv  2713  2moswap  2728  exsnrex  4617  eliunxp  5707  asymref  5974  dffun9  6381  funcnv  6420  funcnv3  6421  f1ompt  6871  eufnfv  6986  dff1o6  7026  dfom2  7570  elxp4  7615  elxp5  7616  abexex  7663  dfoprab4  7744  tpostpos  7903  brwitnlem  8123  erovlem  8383  elixp2  8454  xpsnen  8590  elom3  9100  cardval2  9409  isinfcard  9507  infmap2  9629  elznn0nn  11984  zrevaddcl  12016  qrevaddcl  12360  hash2prb  13820  cotr2g  14326  climreu  14903  isprm3  16017  hashbc0  16331  imasleval  16804  xpscf  16828  isssc  17080  isgim  18332  eldprd  19046  brric2  19420  islmim  19754  tgval2  21483  eltg2b  21486  snfil  22391  isms2  22978  setsms  23008  elii1  23457  phtpcer  23517  elovolm  23994  ellimc2  24393  limcun  24411  1cubr  25336  fsumvma2  25707  dchrelbas3  25731  2lgslem1b  25885  nbgrel  27039  rusgrnumwwlks  27670  isgrpo  28191  mdsl2i  30016  cvmdi  30018  rabfmpunirn  30316  eulerpartlemn  31528  bnj580  32074  bnj1049  32133  snmlval  32465  satf0suclem  32509  fmlasuc0  32518  elmthm  32710  imaindm  32909  dmscut  33159  madeval2  33177  brtxp2  33229  brpprod3a  33234  bj-elid6  34344  ismgmOLD  34999  brres2  35400  brxrn2  35497  redundpim3  35735  prtlem100  35865  islln2  36517  islpln2  36542  islvol2  36586  prjspeclsp  39130  en2pr  39774  pren2  39780  elmapintrab  39804  clcnvlem  39851  sprvalpw  43477  sprvalpwn0  43480  prprvalpw  43512  eliunxp2  44217  elbigo  44446
  Copyright terms: Public domain W3C validator