Theorem pm4.71ri 569

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anabs7  676  biadaniALT  832  orabs  1014  prlem2  1069  dfeumo  2570  dfeu  2629  2moswapv  2663  2moswap  2678  exsnrex  4651  eliunxp  5824  asymref  6117  imaindm  6301  dffun9  6566  funcnv  6606  funcnv3  6607  f1ompt  7107  eufnfv  7228  dff1o6  7274  dfom2  7863  elxp4  7918  elxp5  7919  abexex  7967  dfoprab4  8051  tpostpos  8241  brwitnlem  8491  erovlem  8810  elixp2  8898  xpsnen  9048  elom3  9616  ttrclse  9695  cardval2  9976  isinfcard  10075  infmap2  10199  elznn0nn  12604  zrevaddcl  12638  qrevaddcl  12994  hash2prb  14508  hash3tpb  14531  cotr2g  15012  climreu  15606  isprm3  16740  hashbc0  17064  imasleval  17594  xpscf  17618  isssc  17876  issubmndb  18862  isgim  19331  eldprd  20075  brric2  20588  islmim  21160  tgval2  23081  eltg2b  23084  snfil  23989  isms2  24575  setsms  24605  elii1  25062  phtpcer  25122  elovolm  25602  ellimc2  26004  limcun  26022  1cubr  26972  fsumvma2  27343  dchrelbas3  27367  2lgslem1b  27521  dmcuts  27949  madeval2  27991  made0  28021  nbgrel  29630  rusgrnumwwlks  30266  isgrpo  30789  mdsl2i  32614  cvmdi  32616  rabfmpunirn  32938  zarcls  34208  eulerpartlemn  34715  bnj580  35245  bnj1049  35306  snmlval  35721  satf0suclem  35765  fmlasuc0  35774  elmthm  35966  brtxp2  36269  brpprod3a  36274  bj-elid6  37701  ismgmOLD  38388  brres2  38811  ralmo  38898  brxrn2  38922  dfsuccl4  39012  redundpim3  39252  prtlem100  39522  islln2  40174  islpln2  40199  islvol2  40243  prjspeclsp  43235  onsucrn  43889  dflim5  43947  en2pr  44164  pren2  44170  elmapintrab  44193  clcnvlem  44240  sprvalpw  48117  sprvalpwn0  48120  prprvalpw  48152  clnbgrel  48481  eliunxp2  48998  elbigo  49215