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  574  biadani  614  orabs  819  prlem2  980  sb6  1933  2moswapdc  2168  exsnrex  3708  eliunxp  4861  asymref  5114  elxp4  5216  elxp5  5217  dffun9  5347  funcnv  5382  funcnv3  5383  f1ompt  5788  eufnfv  5874  dff1o6  5906  abexex  6277  dfoprab4  6344  tpostpos  6416  erovlem  6782  elixp2  6857  xpsnen  6988  ctssdccl  7289  ltbtwnnq  7614  enq0enq  7629  prnmaxl  7686  prnminu  7687  elznn0nn  9471  zrevaddcl  9508  qrevaddcl  9851  climreu  11823  isprm3  12655  isprm4  12656  xpscf  13395  tgval2  14740  eltg2b  14743  isms2  15143  2lgslem1b  15783