Theorem syl5ibr 214

Description: A mixed syllogism inference from a nested implication and a biconditional.

Hypotheses

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

Assertion

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

Proof of Theorem syl5ibr

Step	Hyp	Ref	Expression
1		syl5ibr.1	. 2 |- (ph -> (ps -> ch))
2		syl5ibr.2	. . 3 |- (ps <-> th)
3	2	biimpri 159	. 2 |- (th -> ps)
4	1, 3	syl5 21	1 |- (ph -> (th -> ch))

Syntax hints:   -> wi 3   <-> wb 153

This theorem is referenced by:  nicodrawOLD 966  nic-ax 975  a12studyALT 1421  necon4ad 1673  necon1bd 1679  pm2.61dne 1682  rcla4dv 1925  ceqex 1933  ra4esbca 2049  csbie2t 2084  ssdisj 2370  pssdifn0 2381  wereu 3002  ordelord 3027  unizlim 3170  findsg 3214  tfindsg 3219  tfindes 3221  tfinds2 3222  ralxp 3275  cotr 3493  cnvsym 3494  funopfv 3808  funfvima 3909  tz7.49 4017  om00 4264  eceqopreq 4374  th3qlem1 4375  unen 4497  php3 4580  pssnn 4599  isfinite2 4609  fiint 4620  sucprcreg 4660  inf3lem2 4676  setind 4710  rankxplim3 4776  aceq5lem4 4800  kmlem13 4839  zorn2lem4 4853  cardlim 4916  ssxr 5605  arch 6153  xrsupsslem 6158  xrinfmsslem 6159  uzwo3lem2 6302  qbtwnre 6331  ioossicc 6423  fseqsupcl 6551  fseqsupubi 6552  sq01 6740  crulem 6826  cau4ii 7008  cau5i 7009  cvganz 7014  caubndi 7016  bccl 7062  climaddlem3 7206  climmullem8 7217  efseq1ex 7396  infmap2lem1 7671  0ntr 7787  opnneiid 7822  opnin 7954  lmuni 8036  xpcn 8061  bcthlem10 8093  nvmul0or 8356  hvmul0or 8977  hlimcauii 9189  ocnel 9253  spanuni 9550  spansni 9563  h1datomi 9587  hon0 9802  leopadd 10148  leoptr 10153  mdsymlem6 10419  sumdmdlem2 10430  cdjreui 10443  fiiu2 10574  sfseqeq 10637  qusp 10649  iintlem1 10714

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 154

Copyright terms: Public domain