Theorem pm4.71ri 668

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

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

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 385

This theorem is referenced by:  biadan2  677  anabs7  887  orabs  936  prlem2  1044  eu5  2629  2moswap  2681  exsnrex  4361  eliunxp  5411  asymref  5666  dffun9  6074  funcnv  6115  funcnv3  6116  f1ompt  6541  eufnfv  6650  dff1o6  6690  dfom2  7228  elxp4  7271  elxp5  7272  abexex  7312  dfoprab4  7388  tpostpos  7537  brwitnlem  7752  erovlem  8006  elixp2  8074  xpsnen  8205  elom3  8714  cardval2  9003  isinfcard  9101  infmap2  9228  elznn0nn  11579  zrevaddcl  11610  qrevaddcl  11999  hash2prb  13442  cotr2g  13912  climreu  14482  isprm3  15594  hashbc0  15907  imasleval  16399  isssc  16677  isgim  17901  eldprd  18599  brric2  18943  islmim  19260  tgval2  20958  eltg2b  20961  snfil  21865  isms2  22452  setsms  22482  elii1  22931  phtpcer  22991  elovolm  23439  ellimc2  23836  limcun  23854  1cubr  24764  fsumvma2  25134  dchrelbas3  25158  2lgslem1b  25312  nbgrel  26428  rusgrnumwwlks  27092  isgrpo  27656  mdsl2i  29486  cvmdi  29488  rabfmpunirn  29758  eulerpartlemn  30748  bnj580  31286  bnj1049  31345  snmlval  31616  elmthm  31776  imaindm  31983  dmscut  32220  madeval2  32238  brtxp2  32290  brpprod3a  32295  ismgmOLD  33958  brres2  34355  brxrn2  34456  prtlem100  34644  islln2  35296  islpln2  35321  islvol2  35365  elmapintrab  38380  clcnvlem  38428  sprvalpw  42236  sprvalpwn0  42239  eliunxp2  42618  elbigo  42851