Theorem pm4.71ri 392

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biadan2  456  anabs7  576  biadani  616  orabs  822  prlem2  983  sb6  1936  2moswapdc  2171  exsnrex  3731  eliunxp  4894  asymref  5148  elxp4  5250  elxp5  5251  dffun9  5381  funcnv  5417  funcnv3  5418  f1ompt  5828  eufnfv  5917  dff1o6  5949  abexex  6319  dfoprab4  6386  tpostpos  6495  erovlem  6861  elixp2  6937  xpsnen  7072  ctssdccl  7402  ltbtwnnq  7731  enq0enq  7746  prnmaxl  7803  prnminu  7804  elznn0nn  9591  zrevaddcl  9628  qrevaddcl  9976  climreu  11982  isprm3  12815  isprm4  12816  xpscf  13560  tgval2  14916  eltg2b  14919  isms2  15319  2lgslem1b  15962