Theorem syl5bi 208

Description: A mixed syllogism inference.

Hypotheses

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

Assertion

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

Proof of Theorem syl5bi

Step	Hyp	Ref	Expression
1		syl5bi.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimpd 153	. 2 |- (ph -> (ps -> ch))
3		syl5bi.2	. 2 |- (th -> ps)
4	2, 3	syl5 21	1 |- (ph -> (th -> ch))

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

This theorem is referenced by:  syl5cbi 209  ax11indalem 1361  ax11inda2ALT 1362  gencl 1819  a4sbc 1935  hbsbc1g 1938  ssnelpss 2320  prex 2771  opth 2777  sotrieq 2852  ordtri3 2973  brelg 3212  optocl 3225  xpexr 3465  relcnvexb 3507  funimass1 3558  f1ocnvb 3687  tz6.12-2 3724  fnrnfv 3744  eqfnfv 3782  fconst5 3833  funiunfv 3851  f1fv 3859  f1ocnvfv 3865  f1ocnvfvb 3866  oawordeulem 4172  oalimcl 4178  odi 4194  ectocl 4286  eceqopreq 4297  undom 4418  mapdom2 4474  isfinite2 4523  unfi 4528  inf0 4578  rankr1b 4671  rankxplim2 4685  scott0 4689  aceq5 4712  zorn2lem5 4764  zorn2lem6 4765  carduni 4830  axrepndlem2 4917  axunnd 4920  axregnd 4928  mulcanpi 4999  indpi 5006  ltaddpq 5051  nsmallpq 5055  ltbtwnpq 5056  addclprlem1 5090  ltaddpr2 5113  ltaprlem 5122  reclem3pr 5130  supsrlem2 5198  negeu 5327  xrltnet 5538  receu 5670  nnaddclt 5888  nndivtrt 5907  xrsupss 6025  xrinfmss 6026  zmulclt 6127  zeot 6146  zneo 6147  zneoOLD 6148  qnegclt 6208  om2uzlt 6235  uz11t 6364  fzoptht 6434  exple1t 6538  crulem 6666  replimt 6692  bccl2t 6909  infmap2lem2 7522  qdensere 7691  iscms2lem4 7926  grpinveu 7998  grpinvf 8014  iporthcom 8303  eff1i 8665  norm1ex 9043  projlem13 9114  projlem31 9132  dfch2 9164  shmods 9277  shmod 9278  orthin 9285  chssoct 9334  spansncv 9514  adjvalvalt 9777  kbpjt 9796  lnopunilem1 9850  cnlnssadj 9928  strlem4 10091  strlem5 10092  hstrlem4 10099  hstrlem5 10100  dmdmdt 10137  mdslle1 10152  mdslle2 10153  mdslmd1lem1 10160  atcvatlem 10220  atcvat4 10232  mdsymlem3 10240  cayleylem3 10318  fine2 10375  1ded 10515  1cat 10536

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