Theorem pm4.71ri 389

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 387	. 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  451  anabs7  563  biadani  601  orabs  803  prlem2  958  sb6  1858  2moswapdc  2087  exsnrex  3561  eliunxp  4673  asymref  4919  elxp4  5021  elxp5  5022  dffun9  5147  funcnv  5179  funcnv3  5180  f1ompt  5564  eufnfv  5641  dff1o6  5670  abexex  6017  dfoprab4  6083  tpostpos  6154  erovlem  6514  elixp2  6589  xpsnen  6708  ctssdccl  6989  ltbtwnnq  7217  enq0enq  7232  prnmaxl  7289  prnminu  7290  elznn0nn  9061  zrevaddcl  9097  qrevaddcl  9429  climreu  11059  isprm3  11788  isprm4  11789  tgval2  12209  eltg2b  12212  isms2  12612