Theorem pm4.71ri 389

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biadan2  451  anabs7  563  biadani  601  orabs  803  prlem2  958  sb6  1858  2moswapdc  2089  exsnrex  3566  eliunxp  4678  asymref  4924  elxp4  5026  elxp5  5027  dffun9  5152  funcnv  5184  funcnv3  5185  f1ompt  5571  eufnfv  5648  dff1o6  5677  abexex  6024  dfoprab4  6090  tpostpos  6161  erovlem  6521  elixp2  6596  xpsnen  6715  ctssdccl  6996  ltbtwnnq  7224  enq0enq  7239  prnmaxl  7296  prnminu  7297  elznn0nn  9068  zrevaddcl  9104  qrevaddcl  9436  climreu  11066  isprm3  11799  isprm4  11800  tgval2  12220  eltg2b  12223  isms2  12623