Metamath Proof Explorer


Theorem abcdta

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

Ref Expression
Hypothesis abcdta.1 φψχθ
Assertion abcdta φ

Proof

Step Hyp Ref Expression
1 abcdta.1 φψχθ
2 1 simpli φψχ
3 2 simpli φψ
4 3 simpli φ