Theorem pm4.71ri 561

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  anabs7  662  biadaniALT  819  orabs  997  prlem2  1054  dfeumo  2531  dfeu  2589  2moswapv  2625  2moswap  2640  exsnrex  4683  eliunxp  5835  asymref  6114  imaindm  6295  dffun9  6574  funcnv  6614  funcnv3  6615  f1ompt  7107  eufnfv  7227  dff1o6  7269  dfom2  7853  elxp4  7909  elxp5  7910  abexex  7954  dfoprab4  8037  tpostpos  8227  brwitnlem  8503  erovlem  8803  elixp2  8891  xpsnen  9051  elom3  9639  ttrclse  9718  cardval2  9982  isinfcard  10083  infmap2  10209  elznn0nn  12568  zrevaddcl  12603  qrevaddcl  12951  hash2prb  14429  cotr2g  14919  climreu  15496  isprm3  16616  hashbc0  16934  imasleval  17483  xpscf  17507  isssc  17763  issubmndb  18682  isgim  19130  eldprd  19868  brric2  20277  islmim  20665  tgval2  22450  eltg2b  22453  snfil  23359  isms2  23947  setsms  23979  elii1  24442  phtpcer  24502  elovolm  24983  ellimc2  25385  limcun  25403  1cubr  26336  fsumvma2  26706  dchrelbas3  26730  2lgslem1b  26884  dmscut  27301  madeval2  27337  made0  27357  nbgrel  28586  rusgrnumwwlks  29217  isgrpo  29737  mdsl2i  31562  cvmdi  31564  rabfmpunirn  31865  zarcls  32842  eulerpartlemn  33368  bnj580  33912  bnj1049  33973  snmlval  34310  satf0suclem  34354  fmlasuc0  34363  elmthm  34555  brtxp2  34841  brpprod3a  34846  bj-elid6  36039  ismgmOLD  36706  brres2  37124  brxrn2  37233  redundpim3  37488  prtlem100  37717  islln2  38370  islpln2  38395  islvol2  38439  prjspeclsp  41350  onsucrn  42006  dflim5  42064  en2pr  42283  pren2  42289  elmapintrab  42312  clcnvlem  42359  sprvalpw  46134  sprvalpwn0  46137  prprvalpw  46169  eliunxp2  46962  elbigo  47190