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

Metamath Proof Explorer

Theorem dedth

Description: Weak deduction theorem that eliminates a hypothesis ph , making it become an antecedent. We assume that a proof exists for ph when the class variable A is replaced with a specific class B . The hypothesis ch should be assigned to the inference, and the inference hypothesis eliminated with elimhyp . If the inference has other hypotheses with class variable A , these can be kept by assigning keephyp to them. For more information, see the Weak Deduction Theorem page mmdeduction.html . (Contributed by NM, 15-May-1999)

Ref Expression
Hypotheses dedth.1 
|- ( A = if ( ph , A , B ) -> ( ps <-> ch ) )
dedth.2 
|- ch
Assertion dedth 
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 dedth.1 
 |-  ( A = if ( ph , A , B ) -> ( ps <-> ch ) )
2 dedth.2 
 |-  ch
3 iftrue 
 |-  ( ph -> if ( ph , A , B ) = A )
4 3 eqcomd 
 |-  ( ph -> A = if ( ph , A , B ) )
5 4 1 syl 
 |-  ( ph -> ( ps <-> ch ) )
6 2 5 mpbiri 
 |-  ( ph -> ps )