Metamath Proof Explorer

Theorem abcdtd

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

Ref Expression
Hypothesis abcdtd.1 
|- ( ( ( ph /\ ps ) /\ ch ) /\ th )
Assertion abcdtd 
|- th

Proof

Step Hyp Ref Expression
1 abcdtd.1 
 |-  ( ( ( ph /\ ps ) /\ ch ) /\ th )
2 1 simpri 
 |-  th