Metamath Proof Explorer


Theorem syl7

Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 12-Jan-1993) (Proof shortened by Wolf Lammen, 3-Aug-2012)

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

Proof

Step Hyp Ref Expression
1 syl7.1 φψ
2 syl7.2 χθψτ
3 1 a1i χφψ
4 3 2 syl5d χθφτ