Theorem pm4.71ri 396

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biadan2  460  anabs7  580  biadani  620  orabs  826  prlem2  987  sb6  1941  2moswapdc  2177  exsnrex  3751  eliunxp  4921  asymref  5176  elxp4  5278  elxp5  5279  dffun9  5409  funcnv  5445  funcnv3  5446  f1ompt  5862  eufnfv  5952  dff1o6  5985  abexex  6359  dfoprab4  6430  tpostpos  6540  erovlem  6906  elixp2  6990  xpsnen  7125  ctssdccl  7457  ltbtwnnq  7789  enq0enq  7804  prnmaxl  7861  prnminu  7862  elznn0nn  9667  zrevaddcl  9704  qrevaddcl  10059  climreu  12087  isprm3  12920  isprm4  12921  xpscf  13726  tgval2  15294  eltg2b  15297  isms2  15697  2lgslem1b  16430