Theorem pm4.71ri 484

Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed).

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 482	. 2 ⊢ ((φ → ψ) ↔ (φ ↔ (ψ ∧ φ)))
3	1, 2	mpbi 164	1 ⊢ (φ ↔ (ψ ∧ φ))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  2moswap 1064  onzsl 2367  dfom2 2374  elxp4 2640  elxp5 2641  funcnv 2703  f1o3 2805  f1o5 2808  xpsnen 3339  iscard 3659  iscard2 3660  cardval2 3661  isinfcard 3692  elznn0nn 4575  zrevaddclt 4592  elnn0nn 4593  elnnnn0 4594  qrevaddclt 4648  infmap2 4953

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org