Metamath Proof Explorer


Theorem pm4.71ri

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)

Ref Expression
Hypothesis pm4.71ri.1 φ ψ
Assertion pm4.71ri φ ψ φ

Proof

Step Hyp Ref Expression
1 pm4.71ri.1 φ ψ
2 1 pm4.71i φ φ ψ
3 2 biancomi φ ψ φ