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  2531  dfeu  2589  2moswapv  2623  2moswap  2638  exsnrex  4647  eliunxp  5804  asymref  6092  imaindm  6275  dffun9  6548  funcnv  6588  funcnv3  6589  f1ompt  7086  eufnfv  7206  dff1o6  7253  dfom2  7847  elxp4  7901  elxp5  7902  abexex  7953  dfoprab4  8037  tpostpos  8228  brwitnlem  8474  erovlem  8789  elixp2  8877  xpsnen  9029  elom3  9608  ttrclse  9687  cardval2  9951  isinfcard  10052  infmap2  10177  elznn0nn  12550  zrevaddcl  12585  qrevaddcl  12937  hash2prb  14444  hash3tpb  14467  cotr2g  14949  climreu  15529  isprm3  16660  hashbc0  16983  imasleval  17511  xpscf  17535  isssc  17789  issubmndb  18739  isgim  19201  eldprd  19943  brric2  20422  islmim  20976  tgval2  22850  eltg2b  22853  snfil  23758  isms2  24345  setsms  24375  elii1  24838  phtpcer  24901  elovolm  25383  ellimc2  25785  limcun  25803  1cubr  26759  fsumvma2  27132  dchrelbas3  27156  2lgslem1b  27310  dmscut  27730  madeval2  27768  made0  27792  nbgrel  29274  rusgrnumwwlks  29911  isgrpo  30433  mdsl2i  32258  cvmdi  32260  rabfmpunirn  32584  zarcls  33871  eulerpartlemn  34379  bnj580  34910  bnj1049  34971  snmlval  35325  satf0suclem  35369  fmlasuc0  35378  elmthm  35570  brtxp2  35876  brpprod3a  35881  bj-elid6  37165  ismgmOLD  37851  brres2  38264  brxrn2  38364  redundpim3  38628  prtlem100  38859  islln2  39512  islpln2  39537  islvol2  39581  prjspeclsp  42607  onsucrn  43267  dflim5  43325  en2pr  43543  pren2  43549  elmapintrab  43572  clcnvlem  43619  sprvalpw  47485  sprvalpwn0  47488  prprvalpw  47520  clnbgrel  47833  eliunxp2  48326  elbigo  48544