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 951  a12studyALT 1378  necon4ad 1624  necon1bd 1630  pm2.61dne 1633  rcla4dv 1875  ceqex 1883  ra4esbca 1996  csbie2t 2030  ssdisj 2315  pssdifn0 2326  wereu 2941  ordelord 2966  unizlim 3109  findsg 3153  tfindsg 3158  tfindes 3160  tfinds2 3161  ralxp 3214  cotr 3432  cnvsym 3433  funopfv 3746  funfvima 3847  tz7.49 3954  om00 4199  eceqopreq 4306  th3qlem1 4307  unen 4423  php3 4504  pssnn 4522  isfinite2 4532  fiint 4543  sucprcreg 4583  inf3lem2 4597  setind 4631  rankxplim3 4697  aceq5lem4 4721  kmlem13 4760  zorn2lem4 4774  cardlim 4834  ssxr 5523  arch 6028  xrsupsslem 6033  xrinfmsslem 6034  uzwo3lem2 6175  qbtwnre 6228  ioossicc 6343  fseqsupcl 6470  fseqsupub 6471  sq01t 6596  crulem 6681  cau4i 6870  cau5 6871  cvganz 6876  caubnd 6878  bcclt 6925  climaddlem3 7069  climmullem8 7080  efseq1ex 7265  infmap2lem1 7539  0ntr 7662  opnneiid 7697  opnin 7831  lmuni 7913  xpcn 7938  bcthlem10 7970  nvmul0or 8236  hvmul0ort 8849  hlimcaui 9061  ocnelt 9125  spanun 9422  spansn 9436  h1datom 9461  hon0 9676  leopaddt 10021  leoptrt 10026  mdsymlem6 10291  sumdmdlem2 10302  cdjreu 10315  fiiu2 10436  qusp 10489  iintlem1 10548

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