Metamath Proof Explorer

Theorem 3anandis

Description: Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007)

Ref Expression
Hypothesis 3anandis.1 
|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) /\ ( ph /\ th ) ) -> ta )
Assertion 3anandis 
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )

Proof

Step Hyp Ref Expression
1 3anandis.1 
 |-  ( ( ( ph /\ ps ) /\ ( ph /\ ch ) /\ ( ph /\ th ) ) -> ta )
2 simpl 
 |-  ( ( ph /\ ( ps /\ ch /\ th ) ) -> ph )
3 simpr1 
 |-  ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )
4 simpr2 
 |-  ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )
5 simpr3 
 |-  ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )
6 2 3 2 4 2 5 1 syl222anc 
 |-  ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )