Metamath Proof Explorer


Theorem dedth2v

Description: Weak deduction theorem for eliminating a hypothesis with 2 class variables. Note: if the hypothesis can be separated into two hypotheses, each with one class variable, then dedth2h is simpler to use. See also comments in dedth . (Contributed by NM, 13-Aug-1999) (Proof shortened by Eric Schmidt, 28-Jul-2009)

Ref Expression
Hypotheses dedth2v.1 A = if φ A C ψ χ
dedth2v.2 B = if φ B D χ θ
dedth2v.3 θ
Assertion dedth2v φ ψ

Proof

Step Hyp Ref Expression
1 dedth2v.1 A = if φ A C ψ χ
2 dedth2v.2 B = if φ B D χ θ
3 dedth2v.3 θ
4 1 2 3 dedth2h φ φ ψ
5 4 anidms φ ψ