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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anabs7  661  biadaniALT  818  orabs  996  prlem2  1053  dfeumo  2530  dfeu  2588  2moswapv  2624  2moswap  2639  exsnrex  4685  eliunxp  5838  asymref  6118  imaindm  6299  dffun9  6578  funcnv  6618  funcnv3  6619  f1ompt  7113  eufnfv  7234  dff1o6  7276  dfom2  7860  elxp4  7916  elxp5  7917  abexex  7961  dfoprab4  8044  tpostpos  8234  brwitnlem  8510  erovlem  8810  elixp2  8898  xpsnen  9058  elom3  9646  ttrclse  9725  cardval2  9989  isinfcard  10090  infmap2  10216  elznn0nn  12577  zrevaddcl  12612  qrevaddcl  12960  hash2prb  14438  cotr2g  14928  climreu  15505  isprm3  16625  hashbc0  16943  imasleval  17492  xpscf  17516  isssc  17772  issubmndb  18723  isgim  19177  eldprd  19916  brric2  20398  islmim  20818  tgval2  22680  eltg2b  22683  snfil  23589  isms2  24177  setsms  24209  elii1  24679  phtpcer  24742  elovolm  25225  ellimc2  25627  limcun  25645  1cubr  26580  fsumvma2  26950  dchrelbas3  26974  2lgslem1b  27128  dmscut  27546  madeval2  27582  made0  27602  nbgrel  28861  rusgrnumwwlks  29492  isgrpo  30014  mdsl2i  31839  cvmdi  31841  rabfmpunirn  32142  zarcls  33149  eulerpartlemn  33675  bnj580  34219  bnj1049  34280  snmlval  34617  satf0suclem  34661  fmlasuc0  34670  elmthm  34862  brtxp2  35154  brpprod3a  35159  bj-elid6  36355  ismgmOLD  37022  brres2  37440  brxrn2  37549  redundpim3  37804  prtlem100  38033  islln2  38686  islpln2  38711  islvol2  38755  prjspeclsp  41657  onsucrn  42324  dflim5  42382  en2pr  42601  pren2  42607  elmapintrab  42630  clcnvlem  42677  sprvalpw  46448  sprvalpwn0  46451  prprvalpw  46483  eliunxp2  47099  elbigo  47326