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

Metamath Proof Explorer

Theorem iden2

Description: Virtual deduction identity rule. simpr in conjunction form Virtual Deduction notation. (Contributed by Alan Sare, 5-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion iden2 
|- (. (. ph ,. ps ). ->. ps ).

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ph /\ ps ) -> ps )
2 dfvd2an 
 |-  ( (. (. ph ,. ps ). ->. ps ). <-> ( ( ph /\ ps ) -> ps ) )
3 1 2 mpbir 
 |-  (. (. ph ,. ps ). ->. ps ).