Metamath Proof Explorer

Theorem 3an1rs

Description: Swap conjuncts. (Contributed by NM, 16-Dec-2007) (Proof shortened by Wolf Lammen, 14-Apr-2022)

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

Proof

Step Hyp Ref Expression
1 3an1rs.1 
 |-  ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )
2 1 3exp1 
 |-  ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
3 2 com34 
 |-  ( ph -> ( ps -> ( th -> ( ch -> ta ) ) ) )
4 3 3imp1 
 |-  ( ( ( ph /\ ps /\ th ) /\ ch ) -> ta )