Metamath Proof Explorer


Theorem abcdtb

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

Ref Expression
Hypothesis abcdtb.1 ⊢ φ ∧ ψ ∧ χ ∧ θ
Assertion abcdtb ⊢ ψ

Proof

Step Hyp Ref Expression
1 abcdtb.1 ⊢ φ ∧ ψ ∧ χ ∧ θ
2 1 simpli ⊢ φ ∧ ψ ∧ χ
3 2 simpli ⊢ φ ∧ ψ
4 3 simpri ⊢ ψ