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 φψχθ