Metamath Proof Explorer


Theorem 19.35ri

Description: Inference associated with 19.35 . (Contributed by NM, 12-Mar-1993)

Ref Expression
Hypothesis 19.35ri.1 x φ x ψ
Assertion 19.35ri x φ ψ

Proof

Step Hyp Ref Expression
1 19.35ri.1 x φ x ψ
2 19.35 x φ ψ x φ x ψ
3 1 2 mpbir x φ ψ