Theorem pm4.71ri 665

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	. 2 ⊢ (𝜑 → 𝜓)
2		pm4.71r 663	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	mpbi 220	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  biadan2  674  anabs7  852  orabs  900  prlem2  1006  eu5  2496  2moswap  2547  exsnrex  4221  eliunxp  5259  asymref  5512  dffun9  5917  funcnv  5958  funcnv3  5959  f1ompt  6382  eufnfv  6491  dff1o6  6531  dfom2  7067  elxp4  7110  elxp5  7111  abexex  7151  dfoprab4  7225  tpostpos  7372  brwitnlem  7587  erovlem  7843  elixp2  7912  xpsnen  8044  elom3  8545  cardval2  8817  isinfcard  8915  infmap2  9040  elznn0nn  11391  zrevaddcl  11422  qrevaddcl  11810  hash2prb  13254  cotr2g  13715  climreu  14287  isprm3  15396  hashbc0  15709  imasleval  16201  isssc  16480  isgim  17704  eldprd  18403  brric2  18745  islmim  19062  tgval2  20760  eltg2b  20763  snfil  21668  isms2  22255  setsms  22285  elii1  22734  phtpcer  22794  phtpcerOLD  22795  elovolm  23243  ellimc2  23641  limcun  23659  1cubr  24569  fsumvma2  24939  dchrelbas3  24963  2lgslem1b  25117  rusgrnumwwlks  26869  isgrpo  27351  mdsl2i  29181  cvmdi  29183  rabfmpunirn  29453  eulerpartlemn  30443  bnj580  30983  bnj1049  31042  snmlval  31313  elmthm  31473  imaindm  31682  dmscut  31918  madeval2  31936  brtxp2  31988  brpprod3a  31993  ismgmOLD  33649  brres2  34035  prtlem100  34144  islln2  34797  islpln2  34822  islvol2  34866  elmapintrab  37882  clcnvlem  37930  sprvalpw  41730  sprvalpwn0  41733  eliunxp2  42112  elbigo  42345