Metamath Proof Explorer

Theorem in3an

Description: The virtual deduction introduction rule converting the second conjunct of the third virtual hypothesis into the antecedent of the conclusion. exp4a is the non-virtual deduction form of in3an . (Contributed by Alan Sare, 25-Jun-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis in3an.1 φ , ψ , χ θ τ
Assertion in3an φ , ψ , χ θ τ


Step Hyp Ref Expression
1 in3an.1 φ , ψ , χ θ τ
2 1 dfvd3i φ ψ χ θ τ
3 2 exp4a φ ψ χ θ τ
4 3 dfvd3ir φ , ψ , χ θ τ