Metamath Proof Explorer

Theorem pm4.71i

Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of WhiteheadRussell p. 120. (Contributed by NM, 4-Jan-2004)

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


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