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  1935  2moswapdc  2170  exsnrex  3715  eliunxp  4875  asymref  5129  elxp4  5231  elxp5  5232  dffun9  5362  funcnv  5398  funcnv3  5399  f1ompt  5806  eufnfv  5895  dff1o6  5927  abexex  6297  dfoprab4  6364  tpostpos  6473  erovlem  6839  elixp2  6914  xpsnen  7048  ctssdccl  7353  ltbtwnnq  7679  enq0enq  7694  prnmaxl  7751  prnminu  7752  elznn0nn  9537  zrevaddcl  9574  qrevaddcl  9922  climreu  11920  isprm3  12753  isprm4  12754  xpscf  13493  tgval2  14845  eltg2b  14848  isms2  15248  2lgslem1b  15891