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  2536  dfeu  2595  2moswapv  2629  2moswap  2644  exsnrex  4624  eliunxp  5792  asymref  6079  imaindm  6263  dffun9  6527  funcnv  6567  funcnv3  6568  f1ompt  7063  eufnfv  7184  dff1o6  7230  dfom2  7819  elxp4  7873  elxp5  7874  abexex  7924  dfoprab4  8008  tpostpos  8196  brwitnlem  8442  erovlem  8760  elixp2  8849  xpsnen  8999  elom3  9569  ttrclse  9648  cardval2  9915  isinfcard  10014  infmap2  10139  elznn0nn  12538  zrevaddcl  12572  qrevaddcl  12921  hash2prb  14434  hash3tpb  14457  cotr2g  14938  climreu  15518  isprm3  16652  hashbc0  16976  imasleval  17505  xpscf  17529  isssc  17787  issubmndb  18773  isgim  19237  eldprd  19981  brric2  20483  islmim  21057  tgval2  22921  eltg2b  22924  snfil  23829  isms2  24415  setsms  24445  elii1  24902  phtpcer  24962  elovolm  25442  ellimc2  25844  limcun  25862  1cubr  26806  fsumvma2  27177  dchrelbas3  27201  2lgslem1b  27355  dmcuts  27783  madeval2  27825  made0  27855  nbgrel  29409  rusgrnumwwlks  30045  isgrpo  30568  mdsl2i  32393  cvmdi  32395  rabfmpunirn  32726  zarcls  34018  eulerpartlemn  34525  bnj580  35055  bnj1049  35116  snmlval  35513  satf0suclem  35557  fmlasuc0  35566  elmthm  35758  brtxp2  36061  brpprod3a  36066  bj-elid6  37484  ismgmOLD  38171  brres2  38594  ralmo  38681  brxrn2  38705  dfsuccl4  38795  redundpim3  39035  prtlem100  39305  islln2  39957  islpln2  39982  islvol2  40026  prjspeclsp  43045  onsucrn  43699  dflim5  43757  en2pr  43974  pren2  43980  elmapintrab  44003  clcnvlem  44050  sprvalpw  47940  sprvalpwn0  47943  prprvalpw  47975  clnbgrel  48304  eliunxp2  48810  elbigo  49027