Theorem pm4.71ri 564

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anabs7  663  biadaniALT  820  orabs  996  prlem2  1051  dfeumo  2595  dfeu  2656  2moswapv  2691  2moswap  2706  exsnrex  4578  eliunxp  5672  asymref  5943  dffun9  6353  funcnv  6393  funcnv3  6394  f1ompt  6852  eufnfv  6969  dff1o6  7010  dfom2  7562  elxp4  7609  elxp5  7610  abexex  7654  dfoprab4  7735  tpostpos  7895  brwitnlem  8115  erovlem  8376  elixp2  8448  xpsnen  8584  elom3  9095  cardval2  9404  isinfcard  9503  infmap2  9629  elznn0nn  11983  zrevaddcl  12015  qrevaddcl  12358  hash2prb  13826  cotr2g  14327  climreu  14905  isprm3  16017  hashbc0  16331  imasleval  16806  xpscf  16830  isssc  17082  issubmndb  17962  isgim  18394  eldprd  19119  brric2  19493  islmim  19827  tgval2  21561  eltg2b  21564  snfil  22469  isms2  23057  setsms  23087  elii1  23540  phtpcer  23600  elovolm  24079  ellimc2  24480  limcun  24498  1cubr  25428  fsumvma2  25798  dchrelbas3  25822  2lgslem1b  25976  nbgrel  27130  rusgrnumwwlks  27760  isgrpo  28280  mdsl2i  30105  cvmdi  30107  rabfmpunirn  30416  zarcls  31227  eulerpartlemn  31749  bnj580  32295  bnj1049  32356  snmlval  32691  satf0suclem  32735  fmlasuc0  32744  elmthm  32936  imaindm  33135  dmscut  33385  madeval2  33403  brtxp2  33455  brpprod3a  33460  bj-elid6  34585  ismgmOLD  35288  brres2  35689  brxrn2  35787  redundpim3  36025  prtlem100  36155  islln2  36807  islpln2  36832  islvol2  36876  prjspeclsp  39606  en2pr  40246  pren2  40252  elmapintrab  40276  clcnvlem  40323  sprvalpw  43997  sprvalpwn0  44000  prprvalpw  44032  eliunxp2  44735  elbigo  44965