Theorem pm4.71ri 558

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	. 2 ⊢ (𝜑 → 𝜓)
2		pm4.71r 556	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	mpbi 222	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  anabs7  656  biadaniALT  858  biadan2OLD  860  orabs  1028  prlem2  1084  dfeu  2666  2moswap  2726  exsnrex  4440  eliunxp  5491  asymref  5753  dffun9  6151  funcnv  6190  funcnv3  6191  f1ompt  6629  eufnfv  6746  dff1o6  6785  dfom2  7327  elxp4  7371  elxp5  7372  abexex  7410  dfoprab4  7486  tpostpos  7636  brwitnlem  7853  erovlem  8108  elixp2  8178  xpsnen  8312  elom3  8821  cardval2  9129  isinfcard  9227  infmap2  9354  elznn0nn  11717  zrevaddcl  11749  qrevaddcl  12092  hash2prb  13542  cotr2g  14093  climreu  14663  isprm3  15767  hashbc0  16079  imasleval  16553  isssc  16831  isgim  18054  eldprd  18756  brric2  19100  islmim  19420  tgval2  21130  eltg2b  21133  snfil  22037  isms2  22624  setsms  22654  elii1  23103  phtpcer  23163  elovolm  23640  ellimc2  24039  limcun  24057  1cubr  24981  fsumvma2  25351  dchrelbas3  25375  2lgslem1b  25529  nbgrel  26636  rusgrnumwwlks  27302  rusgrnumwwlksOLD  27303  isgrpo  27906  mdsl2i  29735  cvmdi  29737  rabfmpunirn  30001  eulerpartlemn  30987  bnj580  31528  bnj1049  31587  snmlval  31858  elmthm  32018  imaindm  32219  dmscut  32456  madeval2  32474  brtxp2  32526  brpprod3a  32531  ismgmOLD  34190  brres2  34585  brxrn2  34684  redpim3  34918  prtlem100  34933  islln2  35585  islpln2  35610  islvol2  35654  elmapintrab  38722  clcnvlem  38770  sprvalpw  42576  sprvalpwn0  42579  eliunxp2  42958  elbigo  43191