Theorem syl5ibr 207

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	biimpr 152	. 2 |- (th -> ps)
4	1, 3	syl5 21	1 |- (ph -> (th -> ch))

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

This theorem is referenced by:  nicodraw 949  a12studyALT 1372  necon4ad 1618  necon1bd 1624  pm2.61dne 1627  rcla4dv 1869  ceqex 1877  ra4esbca 1989  csbie2t 2023  ssdisj 2308  pssdifn0 2319  wereu 2935  ordelord 2960  unizlim 3103  findsg 3147  tfindsg 3152  tfindes 3154  tfinds2 3155  ralxp 3208  cotr 3420  cnvsym 3421  funopfv 3736  funfvima 3837  tz7.49 3944  om00 4190  eceqopreq 4297  th3qlem1 4298  unen 4414  php3 4495  pssnn 4513  isfinite2 4523  fiint 4534  sucprcreg 4572  inf3lem2 4586  setind 4620  rankxplim3 4686  aceq5lem4 4710  kmlem13 4749  zorn2lem4 4763  cardlim 4823  ssxr 5513  arch 6018  xrsupsslem 6023  xrinfmsslem 6024  uzwo3lem2 6165  qbtwnre 6216  ioossicc 6330  fseqsupcl 6457  fseqsupub 6458  sq01t 6582  crulem 6666  cau4i 6855  cau5 6856  cvganz 6861  caubnd 6863  bcclt 6910  climaddlem3 7052  climmullem8 7063  efseq1ex 7248  infmap2lem1 7521  0ntr 7644  opnneiid 7678  opnin 7809  lmuni 7886  xpcn 7910  bcthlem10 7942  nvmul0or 8212  hvmul0ort 8815  hlimcaui 9027  ocnelt 9086  spanun 9382  spansn 9396  h1datom 9421  hon0 9636  leopaddt 9977  mdsymlem6 10243  sumdmdlem2 10253  cdjreu 10264  fiiu2 10377  qusp 10430  iintlem1 10476

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 147

Copyright terms: Public domain