Theorem pm4.71ri 384

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biadan2  444  anabs7  539  orabs  761  prlem2  916  sb6  1809  2moswapdc  2033  exsnrex  3453  eliunxp  4523  asymref  4760  elxp4  4858  elxp5  4859  dffun9  4980  funcnv  5011  funcnv3  5012  f1ompt  5373  eufnfv  5442  dff1o6  5468  abexex  5805  dfoprab4  5870  tpostpos  5934  erovlem  6286  xpsnen  6387  ltbtwnnq  6738  enq0enq  6753  prnmaxl  6810  prnminu  6811  elznn0nn  8516  zrevaddcl  8552  qrevaddcl  8880  climreu  10355  isprm3  10725  isprm4  10726