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  817  orabs  992  prlem2  1047  dfeumo  2612  dfeu  2674  2moswapv  2707  2moswap  2722  exsnrex  4610  eliunxp  5701  asymref  5969  dffun9  6377  funcnv  6416  funcnv3  6417  f1ompt  6867  eufnfv  6982  dff1o6  7023  dfom2  7571  elxp4  7616  elxp5  7617  abexex  7661  dfoprab4  7742  tpostpos  7901  brwitnlem  8121  erovlem  8382  elixp2  8453  xpsnen  8589  elom3  9099  cardval2  9408  isinfcard  9506  infmap2  9628  elznn0nn  11983  zrevaddcl  12015  qrevaddcl  12358  hash2prb  13818  cotr2g  14324  climreu  14901  isprm3  16015  hashbc0  16329  imasleval  16802  xpscf  16826  isssc  17078  issubmndb  17958  isgim  18340  eldprd  19055  brric2  19429  islmim  19763  tgval2  21492  eltg2b  21495  snfil  22400  isms2  22987  setsms  23017  elii1  23466  phtpcer  23526  elovolm  24003  ellimc2  24402  limcun  24420  1cubr  25347  fsumvma2  25717  dchrelbas3  25741  2lgslem1b  25895  nbgrel  27049  rusgrnumwwlks  27680  isgrpo  28201  mdsl2i  30026  cvmdi  30028  rabfmpunirn  30326  eulerpartlemn  31538  bnj580  32084  bnj1049  32143  snmlval  32475  satf0suclem  32519  fmlasuc0  32528  elmthm  32720  imaindm  32919  dmscut  33169  madeval2  33187  brtxp2  33239  brpprod3a  33244  bj-elid6  34354  ismgmOLD  35009  brres2  35410  brxrn2  35507  redundpim3  35745  prtlem100  35875  islln2  36527  islpln2  36552  islvol2  36596  prjspeclsp  39140  en2pr  39784  pren2  39790  elmapintrab  39814  clcnvlem  39861  sprvalpw  43519  sprvalpwn0  43522  prprvalpw  43554  eliunxp2  44310  elbigo  44539
  Copyright terms: Public domain W3C validator