Metamath Proof Explorer


Theorem sylan9bbr

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995)

Ref Expression
Hypotheses sylan9bbr.1 φψχ
sylan9bbr.2 θχτ
Assertion sylan9bbr θφψτ

Proof

Step Hyp Ref Expression
1 sylan9bbr.1 φψχ
2 sylan9bbr.2 θχτ
3 1 2 sylan9bb φθψτ
4 3 ancoms θφψτ