Metamath Proof Explorer


Theorem syl3an9b

Description: Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995)

Ref Expression
Hypotheses syl3an9b.1 φψχ
syl3an9b.2 θχτ
syl3an9b.3 ητζ
Assertion syl3an9b φθηψζ

Proof

Step Hyp Ref Expression
1 syl3an9b.1 φψχ
2 syl3an9b.2 θχτ
3 syl3an9b.3 ητζ
4 1 2 sylan9bb φθψτ
5 4 3 sylan9bb φθηψζ
6 5 3impa φθηψζ