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  612  orabs  816  prlem2  977  sb6  1911  2moswapdc  2145  exsnrex  3680  eliunxp  4830  asymref  5082  elxp4  5184  elxp5  5185  dffun9  5314  funcnv  5349  funcnv3  5350  f1ompt  5749  eufnfv  5833  dff1o6  5863  abexex  6229  dfoprab4  6296  tpostpos  6368  erovlem  6732  elixp2  6807  xpsnen  6936  ctssdccl  7234  ltbtwnnq  7559  enq0enq  7574  prnmaxl  7631  prnminu  7632  elznn0nn  9416  zrevaddcl  9453  qrevaddcl  9795  climreu  11693  isprm3  12525  isprm4  12526  xpscf  13264  tgval2  14608  eltg2b  14611  isms2  15011  2lgslem1b  15651