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

Metamath Proof Explorer

Theorem ibar

Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995)

Ref Expression
Assertion ibar 
|- ( ph -> ( ps <-> ( ph /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 iba 
 |-  ( ph -> ( ps <-> ( ps /\ ph ) ) )
2 1 biancomd 
 |-  ( ph -> ( ps <-> ( ph /\ ps ) ) )