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  1662  mo3h  2067  necon1bidc  2387  necon4aidc  2403  r19.30dc  2612  ceqex  2852  ssdisj  3464  ralidm  3508  exmid1dc  4178  rexxfrd  4440  sucprcreg  4525  imain  5269  f0rn0  5381  funopfv  5525  mpteqb  5575  funfvima  5715  fliftfun  5763  iinerm  6569  eroveu  6588  th3qlem1  6599  updjudhf  7040  elni2  7251  genpdisj  7460  lttri3  7974  nn0ltexp2  10619  zfz1iso  10750  cau3lem  11052  maxleast  11151  rexanre  11158  climcau  11284  summodc  11320  mertenslem2  11473  prodmodclem2  11514  prodmodc  11515  fprodseq  11520  divgcdcoprmex  12030  prmind2  12048  pcqmul  12231  pcxcl  12239  pcadd  12267  mul4sq  12320  opnneiid  12764  txuni2  12856  txbas  12858  txbasval  12867  txlm  12879  blin2  13032  tgqioo  13147  2sqlem5  13555  bj-charfunr  13652