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  815  prlem2  975  sb6  1896  2moswapdc  2126  exsnrex  3646  eliunxp  4778  asymref  5026  elxp4  5128  elxp5  5129  dffun9  5257  funcnv  5289  funcnv3  5290  f1ompt  5680  eufnfv  5760  dff1o6  5790  abexex  6140  dfoprab4  6206  tpostpos  6278  erovlem  6640  elixp2  6715  xpsnen  6834  ctssdccl  7123  ltbtwnnq  7428  enq0enq  7443  prnmaxl  7500  prnminu  7501  elznn0nn  9280  zrevaddcl  9316  qrevaddcl  9657  climreu  11318  isprm3  12131  isprm4  12132  xpscf  12784  tgval2  13822  eltg2b  13825  isms2  14225