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 ⊢ ( ( 𝜓 ∧ 𝜃 ) → 𝜂 )