Metamath Proof Explorer


Theorem dfvd3ani

Description: Inference form of dfvd3an . (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis dfvd3ani.1 φ ψ χ θ
Assertion dfvd3ani φ ψ χ θ

Proof

Step Hyp Ref Expression
1 dfvd3ani.1 φ ψ χ θ
2 dfvd3an φ ψ χ θ φ ψ χ θ
3 1 2 mpbi φ ψ χ θ