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  2532  dfeu  2590  2moswapv  2624  2moswap  2639  exsnrex  4630  eliunxp  5776  asymref  6062  imaindm  6246  dffun9  6510  funcnv  6550  funcnv3  6551  f1ompt  7044  eufnfv  7163  dff1o6  7209  dfom2  7798  elxp4  7852  elxp5  7853  abexex  7903  dfoprab4  7987  tpostpos  8176  brwitnlem  8422  erovlem  8737  elixp2  8825  xpsnen  8974  elom3  9538  ttrclse  9617  cardval2  9884  isinfcard  9983  infmap2  10108  elznn0nn  12482  zrevaddcl  12517  qrevaddcl  12869  hash2prb  14379  hash3tpb  14402  cotr2g  14883  climreu  15463  isprm3  16594  hashbc0  16917  imasleval  17445  xpscf  17469  isssc  17727  issubmndb  18713  isgim  19174  eldprd  19918  brric2  20421  islmim  20996  tgval2  22871  eltg2b  22874  snfil  23779  isms2  24365  setsms  24395  elii1  24858  phtpcer  24921  elovolm  25403  ellimc2  25805  limcun  25823  1cubr  26779  fsumvma2  27152  dchrelbas3  27176  2lgslem1b  27330  dmscut  27752  madeval2  27794  made0  27818  nbgrel  29318  rusgrnumwwlks  29955  isgrpo  30477  mdsl2i  32302  cvmdi  32304  rabfmpunirn  32635  zarcls  33887  eulerpartlemn  34394  bnj580  34925  bnj1049  34986  snmlval  35375  satf0suclem  35419  fmlasuc0  35428  elmthm  35620  brtxp2  35923  brpprod3a  35928  bj-elid6  37214  ismgmOLD  37900  brres2  38315  brxrn2  38418  dfsuccl4  38497  redundpim3  38736  prtlem100  38968  islln2  39620  islpln2  39645  islvol2  39689  prjspeclsp  42715  onsucrn  43374  dflim5  43432  en2pr  43650  pren2  43656  elmapintrab  43679  clcnvlem  43726  sprvalpw  47590  sprvalpwn0  47593  prprvalpw  47625  clnbgrel  47938  eliunxp2  48444  elbigo  48662