Metamath Proof Explorer


Theorem abcdtc

Description: Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016)

Ref Expression
Hypothesis abcdtc.1 ( ( ( 𝜑𝜓 ) ∧ 𝜒 ) ∧ 𝜃 )
Assertion abcdtc 𝜒

Proof

Step Hyp Ref Expression
1 abcdtc.1 ( ( ( 𝜑𝜓 ) ∧ 𝜒 ) ∧ 𝜃 )
2 1 simpli ( ( 𝜑𝜓 ) ∧ 𝜒 )
3 2 simpri 𝜒