Theorem pm4.71ri 559

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 558	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
3	2	biancomi 461	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  anabs7  660  biadaniALT  817  orabs  995  prlem2  1052  dfeumo  2529  dfeu  2587  2moswapv  2623  2moswap  2638  exsnrex  4683  eliunxp  5836  asymref  6116  imaindm  6297  dffun9  6576  funcnv  6616  funcnv3  6617  f1ompt  7111  eufnfv  7232  dff1o6  7275  dfom2  7859  elxp4  7915  elxp5  7916  abexex  7960  dfoprab4  8043  tpostpos  8233  brwitnlem  8509  erovlem  8809  elixp2  8897  xpsnen  9057  elom3  9645  ttrclse  9724  cardval2  9988  isinfcard  10089  infmap2  10215  elznn0nn  12576  zrevaddcl  12611  qrevaddcl  12959  hash2prb  14437  cotr2g  14927  climreu  15504  isprm3  16624  hashbc0  16942  imasleval  17491  xpscf  17515  isssc  17771  issubmndb  18722  isgim  19176  eldprd  19915  brric2  20397  islmim  20817  tgval2  22679  eltg2b  22682  snfil  23588  isms2  24176  setsms  24208  elii1  24678  phtpcer  24741  elovolm  25224  ellimc2  25626  limcun  25644  1cubr  26583  fsumvma2  26953  dchrelbas3  26977  2lgslem1b  27131  dmscut  27549  madeval2  27585  made0  27605  nbgrel  28864  rusgrnumwwlks  29495  isgrpo  30017  mdsl2i  31842  cvmdi  31844  rabfmpunirn  32145  zarcls  33152  eulerpartlemn  33678  bnj580  34222  bnj1049  34283  snmlval  34620  satf0suclem  34664  fmlasuc0  34673  elmthm  34865  brtxp2  35157  brpprod3a  35162  bj-elid6  36354  ismgmOLD  37021  brres2  37439  brxrn2  37548  redundpim3  37803  prtlem100  38032  islln2  38685  islpln2  38710  islvol2  38754  prjspeclsp  41656  onsucrn  42323  dflim5  42381  en2pr  42600  pren2  42606  elmapintrab  42629  clcnvlem  42676  sprvalpw  46446  sprvalpwn0  46449  prprvalpw  46481  eliunxp2  47097  elbigo  47324