Theorem pm4.71ri 560

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

Step	Hyp	Ref	Expression
1		pm4.71ri.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	pm4.71i 559	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
3	2	biancomi 462	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anabs7  664  biadaniALT  820  orabs  1000  prlem2  1055  dfeumo  2534  dfeu  2593  2moswapv  2627  2moswap  2642  exsnrex  4635  eliunxp  5784  asymref  6071  imaindm  6255  dffun9  6519  funcnv  6559  funcnv3  6560  f1ompt  7054  eufnfv  7173  dff1o6  7219  dfom2  7808  elxp4  7862  elxp5  7863  abexex  7913  dfoprab4  7997  tpostpos  8186  brwitnlem  8432  erovlem  8748  elixp2  8837  xpsnen  8987  elom3  9555  ttrclse  9634  cardval2  9901  isinfcard  10000  infmap2  10125  elznn0nn  12500  zrevaddcl  12534  qrevaddcl  12882  hash2prb  14393  hash3tpb  14416  cotr2g  14897  climreu  15477  isprm3  16608  hashbc0  16931  imasleval  17460  xpscf  17484  isssc  17742  issubmndb  18728  isgim  19189  eldprd  19933  brric2  20437  islmim  21012  tgval2  22898  eltg2b  22901  snfil  23806  isms2  24392  setsms  24422  elii1  24885  phtpcer  24948  elovolm  25430  ellimc2  25832  limcun  25850  1cubr  26806  fsumvma2  27179  dchrelbas3  27203  2lgslem1b  27357  dmscut  27779  madeval2  27821  made0  27845  nbgrel  29362  rusgrnumwwlks  29999  isgrpo  30521  mdsl2i  32346  cvmdi  32348  rabfmpunirn  32680  zarcls  33980  eulerpartlemn  34487  bnj580  35018  bnj1049  35079  snmlval  35474  satf0suclem  35518  fmlasuc0  35527  elmthm  35719  brtxp2  36022  brpprod3a  36027  bj-elid6  37314  ismgmOLD  37990  brres2  38405  brxrn2  38508  dfsuccl4  38587  redundpim3  38826  prtlem100  39058  islln2  39710  islpln2  39735  islvol2  39779  prjspeclsp  42797  onsucrn  43455  dflim5  43513  en2pr  43730  pren2  43736  elmapintrab  43759  clcnvlem  43806  sprvalpw  47668  sprvalpwn0  47671  prprvalpw  47703  clnbgrel  48016  eliunxp2  48522  elbigo  48739