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  663  biadaniALT  820  orabs  999  prlem2  1056  dfeumo  2540  dfeu  2598  2moswapv  2632  2moswap  2647  exsnrex  4704  eliunxp  5862  asymref  6148  imaindm  6330  dffun9  6607  funcnv  6647  funcnv3  6648  f1ompt  7145  eufnfv  7266  dff1o6  7311  dfom2  7905  elxp4  7962  elxp5  7963  abexex  8012  dfoprab4  8096  tpostpos  8287  brwitnlem  8563  erovlem  8871  elixp2  8959  xpsnen  9121  elom3  9717  ttrclse  9796  cardval2  10060  isinfcard  10161  infmap2  10286  elznn0nn  12653  zrevaddcl  12688  qrevaddcl  13036  hash2prb  14521  hash3tpb  14544  cotr2g  15025  climreu  15602  isprm3  16730  hashbc0  17052  imasleval  17601  xpscf  17625  isssc  17881  issubmndb  18840  isgim  19302  eldprd  20048  brric2  20532  islmim  21084  tgval2  22984  eltg2b  22987  snfil  23893  isms2  24481  setsms  24513  elii1  24983  phtpcer  25046  elovolm  25529  ellimc2  25932  limcun  25950  1cubr  26903  fsumvma2  27276  dchrelbas3  27300  2lgslem1b  27454  dmscut  27874  madeval2  27910  made0  27930  nbgrel  29375  rusgrnumwwlks  30007  isgrpo  30529  mdsl2i  32354  cvmdi  32356  rabfmpunirn  32671  zarcls  33820  eulerpartlemn  34346  bnj580  34889  bnj1049  34950  snmlval  35299  satf0suclem  35343  fmlasuc0  35352  elmthm  35544  brtxp2  35845  brpprod3a  35850  bj-elid6  37136  ismgmOLD  37810  brres2  38224  brxrn2  38331  redundpim3  38586  prtlem100  38815  islln2  39468  islpln2  39493  islvol2  39537  prjspeclsp  42567  onsucrn  43233  dflim5  43291  en2pr  43509  pren2  43515  elmapintrab  43538  clcnvlem  43585  sprvalpw  47354  sprvalpwn0  47357  prprvalpw  47389  clnbgrel  47701  eliunxp2  48058  elbigo  48285