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  814  prlem2  974  sb6  1886  2moswapdc  2116  exsnrex  3634  eliunxp  4766  asymref  5014  elxp4  5116  elxp5  5117  dffun9  5245  funcnv  5277  funcnv3  5278  f1ompt  5667  eufnfv  5747  dff1o6  5776  abexex  6126  dfoprab4  6192  tpostpos  6264  erovlem  6626  elixp2  6701  xpsnen  6820  ctssdccl  7109  ltbtwnnq  7414  enq0enq  7429  prnmaxl  7486  prnminu  7487  elznn0nn  9266  zrevaddcl  9302  qrevaddcl  9643  climreu  11304  isprm3  12117  isprm4  12118  xpscf  12765  tgval2  13521  eltg2b  13524  isms2  13924