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  4763  asymref  5011  elxp4  5113  elxp5  5114  dffun9  5242  funcnv  5274  funcnv3  5275  f1ompt  5664  eufnfv  5743  dff1o6  5772  abexex  6122  dfoprab4  6188  tpostpos  6260  erovlem  6622  elixp2  6697  xpsnen  6816  ctssdccl  7105  ltbtwnnq  7410  enq0enq  7425  prnmaxl  7482  prnminu  7483  elznn0nn  9261  zrevaddcl  9297  qrevaddcl  9638  climreu  11296  isprm3  12108  isprm4  12109  tgval2  13333  eltg2b  13336  isms2  13736