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 ) |
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 ) |