Theorem syl5bir 152

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 132	. 2 |- ( ph -> ps )
3		syl5bir.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	syl5 32	1 |- ( ch -> ( ph -> th ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3g  203  19.37-1  1653  mo3h  2053  necon1bidc  2361  necon4aidc  2377  ceqex  2816  ssdisj  3424  ralidm  3468  exmid1dc  4131  rexxfrd  4392  sucprcreg  4472  imain  5213  f0rn0  5325  funopfv  5469  mpteqb  5519  funfvima  5657  fliftfun  5705  iinerm  6509  eroveu  6528  th3qlem1  6539  updjudhf  6972  elni2  7146  genpdisj  7355  lttri3  7868  zfz1iso  10616  cau3lem  10918  maxleast  11017  rexanre  11024  climcau  11148  summodc  11184  mertenslem2  11337  prodmodclem2  11378  prodmodc  11379  fprodseq  11384  divgcdcoprmex  11819  prmind2  11837  opnneiid  12372  txuni2  12464  txbas  12466  txbasval  12475  txlm  12487  blin2  12640  tgqioo  12755