Metamath Proof Explorer


Theorem eel11111

Description: Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 eel11111.1 ( 𝜑𝜓 )
2 eel11111.2 ( 𝜑𝜒 )
3 eel11111.3 ( 𝜑𝜃 )
4 eel11111.4 ( 𝜑𝜏 )
5 eel11111.5 ( 𝜑𝜂 )
6 eel11111.6 ( ( ( ( ( 𝜓𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) → 𝜁 )
7 6 exp41 ( ( 𝜓𝜒 ) → ( 𝜃 → ( 𝜏 → ( 𝜂𝜁 ) ) ) )
8 7 ex ( 𝜓 → ( 𝜒 → ( 𝜃 → ( 𝜏 → ( 𝜂𝜁 ) ) ) ) )
9 1 2 3 8 syl3c ( 𝜑 → ( 𝜏 → ( 𝜂𝜁 ) ) )
10 4 5 9 mp2d ( 𝜑𝜁 )