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  1937  2moswapdc  2173  exsnrex  3736  eliunxp  4899  asymref  5153  elxp4  5255  elxp5  5256  dffun9  5386  funcnv  5422  funcnv3  5423  f1ompt  5833  eufnfv  5922  dff1o6  5955  abexex  6328  dfoprab4  6399  tpostpos  6508  erovlem  6874  elixp2  6950  xpsnen  7085  ctssdccl  7415  ltbtwnnq  7747  enq0enq  7762  prnmaxl  7819  prnminu  7820  elznn0nn  9608  zrevaddcl  9645  qrevaddcl  9994  climreu  12007  isprm3  12840  isprm4  12841  xpscf  13611  tgval2  15042  eltg2b  15045  isms2  15445  2lgslem1b  16088