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  664  biadaniALT  820  orabs  1000  prlem2  1055  dfeumo  2530  dfeu  2588  2moswapv  2622  2moswap  2637  exsnrex  4630  eliunxp  5774  asymref  6059  imaindm  6241  dffun9  6505  funcnv  6545  funcnv3  6546  f1ompt  7038  eufnfv  7157  dff1o6  7203  dfom2  7792  elxp4  7846  elxp5  7847  abexex  7897  dfoprab4  7981  tpostpos  8170  brwitnlem  8416  erovlem  8731  elixp2  8819  xpsnen  8968  elom3  9532  ttrclse  9611  cardval2  9875  isinfcard  9974  infmap2  10099  elznn0nn  12473  zrevaddcl  12508  qrevaddcl  12860  hash2prb  14367  hash3tpb  14390  cotr2g  14870  climreu  15450  isprm3  16581  hashbc0  16904  imasleval  17432  xpscf  17456  isssc  17714  issubmndb  18666  isgim  19128  eldprd  19872  brric2  20375  islmim  20950  tgval2  22825  eltg2b  22828  snfil  23733  isms2  24319  setsms  24349  elii1  24812  phtpcer  24875  elovolm  25357  ellimc2  25759  limcun  25777  1cubr  26733  fsumvma2  27106  dchrelbas3  27130  2lgslem1b  27284  dmscut  27706  madeval2  27748  made0  27772  nbgrel  29272  rusgrnumwwlks  29906  isgrpo  30428  mdsl2i  32253  cvmdi  32255  rabfmpunirn  32587  zarcls  33855  eulerpartlemn  34362  bnj580  34893  bnj1049  34954  snmlval  35321  satf0suclem  35365  fmlasuc0  35374  elmthm  35566  brtxp2  35872  brpprod3a  35877  bj-elid6  37161  ismgmOLD  37847  brres2  38260  brxrn2  38360  redundpim3  38624  prtlem100  38855  islln2  39507  islpln2  39532  islvol2  39576  prjspeclsp  42602  onsucrn  43261  dflim5  43319  en2pr  43537  pren2  43543  elmapintrab  43566  clcnvlem  43613  sprvalpw  47478  sprvalpwn0  47481  prprvalpw  47513  clnbgrel  47826  eliunxp2  48332  elbigo  48550