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  1609  mo3h  2001  necon1bidc  2307  necon4aidc  2323  ceqex  2744  ssdisj  3339  ralidm  3382  rexxfrd  4285  sucprcreg  4365  imain  5096  f0rn0  5205  funopfv  5344  mpteqb  5393  funfvima  5526  fliftfun  5575  iinerm  6364  eroveu  6383  th3qlem1  6394  updjudhf  6770  elni2  6873  genpdisj  7082  lttri3  7565  zfz1iso  10246  cau3lem  10547  maxleast  10646  rexanre  10653  climcau  10736  isummo  10773  mertenslem2  10930  divgcdcoprmex  11362  prmind2  11380