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  1667  mo3h  2072  necon1bidc  2392  necon4aidc  2408  r19.30dc  2617  ceqex  2857  ssdisj  3471  ralidm  3515  exmid1dc  4186  rexxfrd  4448  sucprcreg  4533  imain  5280  f0rn0  5392  funopfv  5536  mpteqb  5586  funfvima  5727  fliftfun  5775  iinerm  6585  eroveu  6604  th3qlem1  6615  updjudhf  7056  elni2  7276  genpdisj  7485  lttri3  7999  nn0ltexp2  10644  zfz1iso  10776  cau3lem  11078  maxleast  11177  rexanre  11184  climcau  11310  summodc  11346  mertenslem2  11499  prodmodclem2  11540  prodmodc  11541  fprodseq  11546  divgcdcoprmex  12056  prmind2  12074  pcqmul  12257  pcxcl  12265  pcadd  12293  mul4sq  12346  opnneiid  12958  txuni2  13050  txbas  13052  txbasval  13061  txlm  13073  blin2  13226  tgqioo  13341  2sqlem5  13749  bj-charfunr  13845