Metamath Proof Explorer


Theorem 4animp1

Description: A single hypothesis unification deduction with an assertion which is an implication with a 4-right-nested conjunction antecedent. (Contributed by Alan Sare, 30-May-2018)

Ref Expression
Hypothesis 4animp1.1
|- ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) )
Assertion 4animp1
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )

Proof

Step Hyp Ref Expression
1 4animp1.1
 |-  ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) )
2 simpr
 |-  ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> th )
3 1 ad4ant123
 |-  ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ( ta <-> th ) )
4 2 3 mpbird
 |-  ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )