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  665  biadaniALT  821  orabs  1001  prlem2  1056  dfeumo  2537  dfeu  2596  2moswapv  2630  2moswap  2645  exsnrex  4625  eliunxp  5787  asymref  6074  imaindm  6258  dffun9  6522  funcnv  6562  funcnv3  6563  f1ompt  7058  eufnfv  7178  dff1o6  7224  dfom2  7813  elxp4  7867  elxp5  7868  abexex  7918  dfoprab4  8002  tpostpos  8190  brwitnlem  8436  erovlem  8754  elixp2  8843  xpsnen  8993  elom3  9563  ttrclse  9642  cardval2  9909  isinfcard  10008  infmap2  10133  elznn0nn  12532  zrevaddcl  12566  qrevaddcl  12915  hash2prb  14428  hash3tpb  14451  cotr2g  14932  climreu  15512  isprm3  16646  hashbc0  16970  imasleval  17499  xpscf  17523  isssc  17781  issubmndb  18767  isgim  19231  eldprd  19975  brric2  20477  islmim  21052  tgval2  22934  eltg2b  22937  snfil  23842  isms2  24428  setsms  24458  elii1  24915  phtpcer  24975  elovolm  25455  ellimc2  25857  limcun  25875  1cubr  26822  fsumvma2  27194  dchrelbas3  27218  2lgslem1b  27372  dmcuts  27800  madeval2  27842  made0  27872  nbgrel  29426  rusgrnumwwlks  30063  isgrpo  30586  mdsl2i  32411  cvmdi  32413  rabfmpunirn  32744  zarcls  34037  eulerpartlemn  34544  bnj580  35074  bnj1049  35135  snmlval  35532  satf0suclem  35576  fmlasuc0  35585  elmthm  35777  brtxp2  36080  brpprod3a  36085  bj-elid6  37503  ismgmOLD  38188  brres2  38611  ralmo  38698  brxrn2  38722  dfsuccl4  38812  redundpim3  39052  prtlem100  39322  islln2  39974  islpln2  39999  islvol2  40043  prjspeclsp  43062  onsucrn  43720  dflim5  43778  en2pr  43995  pren2  44001  elmapintrab  44024  clcnvlem  44071  sprvalpw  47955  sprvalpwn0  47958  prprvalpw  47990  clnbgrel  48319  eliunxp2  48825  elbigo  49042