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  4640  eliunxp  5791  asymref  6077  imaindm  6260  dffun9  6529  funcnv  6569  funcnv3  6570  f1ompt  7065  eufnfv  7185  dff1o6  7232  dfom2  7824  elxp4  7878  elxp5  7879  abexex  7929  dfoprab4  8013  tpostpos  8202  brwitnlem  8448  erovlem  8763  elixp2  8851  xpsnen  9002  elom3  9577  ttrclse  9656  cardval2  9920  isinfcard  10021  infmap2  10146  elznn0nn  12519  zrevaddcl  12554  qrevaddcl  12906  hash2prb  14413  hash3tpb  14436  cotr2g  14918  climreu  15498  isprm3  16629  hashbc0  16952  imasleval  17480  xpscf  17504  isssc  17762  issubmndb  18714  isgim  19176  eldprd  19920  brric2  20426  islmim  21001  tgval2  22876  eltg2b  22879  snfil  23784  isms2  24371  setsms  24401  elii1  24864  phtpcer  24927  elovolm  25409  ellimc2  25811  limcun  25829  1cubr  26785  fsumvma2  27158  dchrelbas3  27182  2lgslem1b  27336  dmscut  27757  madeval2  27798  made0  27822  nbgrel  29320  rusgrnumwwlks  29954  isgrpo  30476  mdsl2i  32301  cvmdi  32303  rabfmpunirn  32627  zarcls  33857  eulerpartlemn  34365  bnj580  34896  bnj1049  34957  snmlval  35311  satf0suclem  35355  fmlasuc0  35364  elmthm  35556  brtxp2  35862  brpprod3a  35867  bj-elid6  37151  ismgmOLD  37837  brres2  38250  brxrn2  38350  redundpim3  38614  prtlem100  38845  islln2  39498  islpln2  39523  islvol2  39567  prjspeclsp  42593  onsucrn  43253  dflim5  43311  en2pr  43529  pren2  43535  elmapintrab  43558  clcnvlem  43605  sprvalpw  47474  sprvalpwn0  47477  prprvalpw  47509  clnbgrel  47822  eliunxp2  48315  elbigo  48533