This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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