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

Metamath Proof Explorer

Theorem mpsyl4anc

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

Ref Expression
Hypotheses mpsyl4anc.1 ⊢ 𝜑
mpsyl4anc.2 ⊢ 𝜓
mpsyl4anc.3 ⊢ 𝜒
mpsyl4anc.4 ⊢ ( 𝜃 → 𝜏 )
mpsyl4anc.5 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜏 ) → 𝜂 )
Assertion mpsyl4anc ( 𝜃 → 𝜂 )

Proof

Step Hyp Ref Expression
1 mpsyl4anc.1 ⊢ 𝜑
2 mpsyl4anc.2 ⊢ 𝜓
3 mpsyl4anc.3 ⊢ 𝜒
4 mpsyl4anc.4 ⊢ ( 𝜃 → 𝜏 )
5 mpsyl4anc.5 ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜏 ) → 𝜂 )
6 1 a1i ⊢ ( 𝜃 → 𝜑 )
7 2 a1i ⊢ ( 𝜃 → 𝜓 )
8 3 a1i ⊢ ( 𝜃 → 𝜒 )
9 6 7 8 4 5 syl1111anc ⊢ ( 𝜃 → 𝜂 )