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  4639  eliunxp  5794  asymref  6081  imaindm  6265  dffun9  6529  funcnv  6569  funcnv3  6570  f1ompt  7065  eufnfv  7185  dff1o6  7231  dfom2  7820  elxp4  7874  elxp5  7875  abexex  7925  dfoprab4  8009  tpostpos  8198  brwitnlem  8444  erovlem  8762  elixp2  8851  xpsnen  9001  elom3  9569  ttrclse  9648  cardval2  9915  isinfcard  10014  infmap2  10139  elznn0nn  12514  zrevaddcl  12548  qrevaddcl  12896  hash2prb  14407  hash3tpb  14430  cotr2g  14911  climreu  15491  isprm3  16622  hashbc0  16945  imasleval  17474  xpscf  17498  isssc  17756  issubmndb  18742  isgim  19203  eldprd  19947  brric2  20451  islmim  21026  tgval2  22912  eltg2b  22915  snfil  23820  isms2  24406  setsms  24436  elii1  24899  phtpcer  24962  elovolm  25444  ellimc2  25846  limcun  25864  1cubr  26820  fsumvma2  27193  dchrelbas3  27217  2lgslem1b  27371  dmcuts  27799  madeval2  27841  made0  27871  nbgrel  29425  rusgrnumwwlks  30062  isgrpo  30585  mdsl2i  32410  cvmdi  32412  rabfmpunirn  32743  zarcls  34052  eulerpartlemn  34559  bnj580  35089  bnj1049  35150  snmlval  35547  satf0suclem  35591  fmlasuc0  35600  elmthm  35792  brtxp2  36095  brpprod3a  36100  bj-elid6  37425  ismgmOLD  38101  brres2  38524  ralmo  38611  brxrn2  38635  dfsuccl4  38725  redundpim3  38965  prtlem100  39235  islln2  39887  islpln2  39912  islvol2  39956  prjspeclsp  42970  onsucrn  43628  dflim5  43686  en2pr  43903  pren2  43909  elmapintrab  43932  clcnvlem  43979  sprvalpw  47840  sprvalpwn0  47843  prprvalpw  47875  clnbgrel  48188  eliunxp2  48694  elbigo  48911