This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mp3an2ani

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017)

Ref Expression
Hypotheses mp3an2ani.1 ⊢ φ
mp3an2ani.2 ⊢ ψ → χ
mp3an2ani.3 ⊢ ψ ∧ θ → τ
mp3an2ani.4 ⊢ φ ∧ χ ∧ τ → η
Assertion mp3an2ani ⊢ ψ ∧ θ → η

Proof

Step Hyp Ref Expression
1 mp3an2ani.1 ⊢ φ
2 mp3an2ani.2 ⊢ ψ → χ
3 mp3an2ani.3 ⊢ ψ ∧ θ → τ
4 mp3an2ani.4 ⊢ φ ∧ χ ∧ τ → η
5 1 2 3 4 mp3an3an ⊢ ψ ∧ ψ ∧ θ → η
6 5 anabss5 ⊢ ψ ∧ θ → η