Theorem syl5bir 151

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5bir.1	|- ( ps <-> ph )
syl5bir.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
syl5bir	|- ( ch -> ( ph -> th ) )

Proof of Theorem syl5bir

Step	Hyp	Ref	Expression
1		syl5bir.1	. . 3 |- ( ps <-> ph )
2	1	biimpri 131	. 2 |- ( ph -> ps )
3		syl5bir.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	syl5 32	1 |- ( ch -> ( ph -> th ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr3g  202  19.37-1  1605  mo3h  1995  necon1bidc  2298  necon4aidc  2314  ceqex  2723  ssdisj  3307  ralidm  3349  rexxfrd  4221  sucprcreg  4300  imain  5012  funopfv  5245  mpteqb  5293  funfvima  5422  fliftfun  5467  iinerm  6244  eroveu  6263  th3qlem1  6274  elni2  6566  genpdisj  6775  lttri3  7258  cau3lem  10138  maxleast  10237  rexanre  10244  climcau  10322  divgcdcoprmex  10628  prmind2  10646