Theorem pm4.71ri 561

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

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

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 397

This theorem is referenced by:  anabs7  662  biadaniALT  819  orabs  997  prlem2  1054  dfeumo  2530  dfeu  2588  2moswapv  2624  2moswap  2639  exsnrex  4646  eliunxp  5798  asymref  6075  imaindm  6256  dffun9  6535  funcnv  6575  funcnv3  6576  f1ompt  7064  eufnfv  7184  dff1o6  7226  dfom2  7809  elxp4  7864  elxp5  7865  abexex  7909  dfoprab4  7992  tpostpos  8182  brwitnlem  8458  erovlem  8759  elixp2  8846  xpsnen  9006  elom3  9593  ttrclse  9672  cardval2  9936  isinfcard  10037  infmap2  10163  elznn0nn  12522  zrevaddcl  12557  qrevaddcl  12905  hash2prb  14383  cotr2g  14873  climreu  15450  isprm3  16570  hashbc0  16888  imasleval  17437  xpscf  17461  isssc  17717  issubmndb  18630  isgim  19066  eldprd  19797  brric2  20195  islmim  20580  tgval2  22343  eltg2b  22346  snfil  23252  isms2  23840  setsms  23872  elii1  24335  phtpcer  24395  elovolm  24876  ellimc2  25278  limcun  25296  1cubr  26229  fsumvma2  26599  dchrelbas3  26623  2lgslem1b  26777  dmscut  27193  madeval2  27226  made0  27246  nbgrel  28351  rusgrnumwwlks  28982  isgrpo  29502  mdsl2i  31327  cvmdi  31329  rabfmpunirn  31636  zarcls  32544  eulerpartlemn  33070  bnj580  33614  bnj1049  33675  snmlval  34012  satf0suclem  34056  fmlasuc0  34065  elmthm  34257  brtxp2  34542  brpprod3a  34547  bj-elid6  35714  ismgmOLD  36382  brres2  36801  brxrn2  36910  redundpim3  37165  prtlem100  37394  islln2  38047  islpln2  38072  islvol2  38116  prjspeclsp  41008  onsucrn  41664  dflim5  41722  en2pr  41941  pren2  41947  elmapintrab  41970  clcnvlem  42017  sprvalpw  45792  sprvalpwn0  45795  prprvalpw  45827  eliunxp2  46529  elbigo  46757