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  4644  eliunxp  5801  asymref  6089  imaindm  6272  dffun9  6545  funcnv  6585  funcnv3  6586  f1ompt  7083  eufnfv  7203  dff1o6  7250  dfom2  7844  elxp4  7898  elxp5  7899  abexex  7950  dfoprab4  8034  tpostpos  8225  brwitnlem  8471  erovlem  8786  elixp2  8874  xpsnen  9025  elom3  9601  ttrclse  9680  cardval2  9944  isinfcard  10045  infmap2  10170  elznn0nn  12543  zrevaddcl  12578  qrevaddcl  12930  hash2prb  14437  hash3tpb  14460  cotr2g  14942  climreu  15522  isprm3  16653  hashbc0  16976  imasleval  17504  xpscf  17528  isssc  17782  issubmndb  18732  isgim  19194  eldprd  19936  brric2  20415  islmim  20969  tgval2  22843  eltg2b  22846  snfil  23751  isms2  24338  setsms  24368  elii1  24831  phtpcer  24894  elovolm  25376  ellimc2  25778  limcun  25796  1cubr  26752  fsumvma2  27125  dchrelbas3  27149  2lgslem1b  27303  dmscut  27723  madeval2  27761  made0  27785  nbgrel  29267  rusgrnumwwlks  29904  isgrpo  30426  mdsl2i  32251  cvmdi  32253  rabfmpunirn  32577  zarcls  33864  eulerpartlemn  34372  bnj580  34903  bnj1049  34964  snmlval  35318  satf0suclem  35362  fmlasuc0  35371  elmthm  35563  brtxp2  35869  brpprod3a  35874  bj-elid6  37158  ismgmOLD  37844  brres2  38257  brxrn2  38357  redundpim3  38621  prtlem100  38852  islln2  39505  islpln2  39530  islvol2  39574  prjspeclsp  42600  onsucrn  43260  dflim5  43318  en2pr  43536  pren2  43542  elmapintrab  43565  clcnvlem  43612  sprvalpw  47481  sprvalpwn0  47484  prprvalpw  47516  clnbgrel  47829  eliunxp2  48322  elbigo  48540