Metamath Proof Explorer

Theorem anim12d1

Description: Variant of anim12d where the second implication does not depend on the antecedent. (Contributed by Rodolfo Medina, 12-Oct-2010)

Ref Expression
Hypotheses anim12d1.1 φ ψ χ
anim12d1.2 θ τ
Assertion anim12d1 φ ψ θ χ τ


Step Hyp Ref Expression
1 anim12d1.1 φ ψ χ
2 anim12d1.2 θ τ
3 2 a1i φ θ τ
4 1 3 anim12d φ ψ θ χ τ