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
|- ( ph -> ps )
Assertion pm4.71i
|- ( ph <-> ( ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 pm4.71i.1
 |-  ( ph -> ps )
2 pm4.71
 |-  ( ( ph -> ps ) <-> ( ph <-> ( ph /\ ps ) ) )
3 1 2 mpbi
 |-  ( ph <-> ( ph /\ ps ) )