Metamath Proof Explorer


Theorem bj-syl66ib

Description: A mixed syllogism inference derived from syl6ib . In addition to bj-dvelimdv1 , it can also shorten alexsubALTlem4 (4821>4812), supsrlem (2868>2863). (Contributed by BJ, 20-Oct-2021)

Ref Expression
Hypotheses bj-syl66ib.1
|- ( ph -> ( ps -> th ) )
bj-syl66ib.2
|- ( th -> ta )
bj-syl66ib.3
|- ( ta <-> ch )
Assertion bj-syl66ib
|- ( ph -> ( ps -> ch ) )

Proof

Step Hyp Ref Expression
1 bj-syl66ib.1
 |-  ( ph -> ( ps -> th ) )
2 bj-syl66ib.2
 |-  ( th -> ta )
3 bj-syl66ib.3
 |-  ( ta <-> ch )
4 1 2 syl6
 |-  ( ph -> ( ps -> ta ) )
5 4 3 syl6ib
 |-  ( ph -> ( ps -> ch ) )