Theorem pm4.71ri 390

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 388	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑)))
3	1, 2	mpbi 144	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biadan2  452  anabs7  564  biadani  602  orabs  804  prlem2  964  sb6  1874  2moswapdc  2104  exsnrex  3618  eliunxp  4743  asymref  4989  elxp4  5091  elxp5  5092  dffun9  5217  funcnv  5249  funcnv3  5250  f1ompt  5636  eufnfv  5715  dff1o6  5744  abexex  6094  dfoprab4  6160  tpostpos  6232  erovlem  6593  elixp2  6668  xpsnen  6787  ctssdccl  7076  ltbtwnnq  7357  enq0enq  7372  prnmaxl  7429  prnminu  7430  elznn0nn  9205  zrevaddcl  9241  qrevaddcl  9582  climreu  11238  isprm3  12050  isprm4  12051  tgval2  12691  eltg2b  12694  isms2  13094