Metamath Proof Explorer

Theorem 3anandirs

Description: Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006)

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

Proof

Step Hyp Ref Expression
1 3anandirs.1 
 |-  ( ( ( ph /\ th ) /\ ( ps /\ th ) /\ ( ch /\ th ) ) -> ta )
2 simpl1 
 |-  ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )
3 simpr 
 |-  ( ( ( ph /\ ps /\ ch ) /\ th ) -> th )
4 simpl2 
 |-  ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
5 simpl3 
 |-  ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
6 2 3 4 3 5 3 1 syl222anc 
 |-  ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )