Theorem pm4.71ri 562

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 561	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
3	2	biancomi 464	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anabs7  663  biadaniALT  820  orabs  998  prlem2  1055  dfeumo  2532  dfeu  2590  2moswapv  2626  2moswap  2641  exsnrex  4685  eliunxp  5838  asymref  6118  imaindm  6299  dffun9  6578  funcnv  6618  funcnv3  6619  f1ompt  7111  eufnfv  7231  dff1o6  7273  dfom2  7857  elxp4  7913  elxp5  7914  abexex  7958  dfoprab4  8041  tpostpos  8231  brwitnlem  8507  erovlem  8807  elixp2  8895  xpsnen  9055  elom3  9643  ttrclse  9722  cardval2  9986  isinfcard  10087  infmap2  10213  elznn0nn  12572  zrevaddcl  12607  qrevaddcl  12955  hash2prb  14433  cotr2g  14923  climreu  15500  isprm3  16620  hashbc0  16938  imasleval  17487  xpscf  17511  isssc  17767  issubmndb  18686  isgim  19136  eldprd  19874  brric2  20285  islmim  20673  tgval2  22459  eltg2b  22462  snfil  23368  isms2  23956  setsms  23988  elii1  24451  phtpcer  24511  elovolm  24992  ellimc2  25394  limcun  25412  1cubr  26347  fsumvma2  26717  dchrelbas3  26741  2lgslem1b  26895  dmscut  27312  madeval2  27348  made0  27368  nbgrel  28597  rusgrnumwwlks  29228  isgrpo  29750  mdsl2i  31575  cvmdi  31577  rabfmpunirn  31878  zarcls  32854  eulerpartlemn  33380  bnj580  33924  bnj1049  33985  snmlval  34322  satf0suclem  34366  fmlasuc0  34375  elmthm  34567  brtxp2  34853  brpprod3a  34858  bj-elid6  36051  ismgmOLD  36718  brres2  37136  brxrn2  37245  redundpim3  37500  prtlem100  37729  islln2  38382  islpln2  38407  islvol2  38451  prjspeclsp  41354  onsucrn  42021  dflim5  42079  en2pr  42298  pren2  42304  elmapintrab  42327  clcnvlem  42374  sprvalpw  46148  sprvalpwn0  46151  prprvalpw  46183  eliunxp2  47009  elbigo  47237