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  453  anabs7  569  biadani  607  orabs  809  prlem2  969  sb6  1879  2moswapdc  2109  exsnrex  3623  eliunxp  4748  asymref  4994  elxp4  5096  elxp5  5097  dffun9  5225  funcnv  5257  funcnv3  5258  f1ompt  5645  eufnfv  5724  dff1o6  5753  abexex  6103  dfoprab4  6169  tpostpos  6241  erovlem  6603  elixp2  6678  xpsnen  6797  ctssdccl  7086  ltbtwnnq  7371  enq0enq  7386  prnmaxl  7443  prnminu  7444  elznn0nn  9219  zrevaddcl  9255  qrevaddcl  9596  climreu  11253  isprm3  12065  isprm4  12066  tgval2  12810  eltg2b  12813  isms2  13213