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 1366  ax11inda2ALT 1367  gencl 1824  a4sbc 1941  hbsbc1g 1944  ssnelpss 2326  prex 2776  opth 2782  sotrieq 2856  ordtri3 2978  brelg 3217  optocl 3230  xpexr 3471  relcnvexb 3513  funimass1 3564  f1ocnvb 3693  tz6.12-2 3730  fnrnfv 3750  eqfnfv 3788  fconst5 3839  funiunfv 3857  f1fv 3865  f1ocnvfv 3871  f1ocnvfvb 3872  oawordeulem 4178  oalimcl 4184  odi 4200  ectocl 4292  eceqopreq 4303  undom 4424  mapdom2 4480  isfinite2 4529  unfi 4534  inf0 4586  rankr1b 4679  rankxplim2 4693  scott0 4697  aceq5 4720  zorn2lem5 4772  zorn2lem6 4773  carduni 4838  axrepndlem2 4925  axunnd 4928  axregnd 4936  mulcanpi 5007  indpi 5014  ltaddpq 5059  nsmallpq 5063  ltbtwnpq 5064  addclprlem1 5098  ltaddpr2 5121  ltaprlem 5130  reclem3pr 5138  supsrlem2 5206  negeu 5335  xrltnet 5546  receu 5678  nnaddclt 5896  nndivtrt 5915  xrsupss 6033  xrinfmss 6034  zmulclt 6135  zeot 6154  zneo 6155  zneoOLD 6156  qnegclt 6216  om2uzlt 6243  uz11t 6372  fzoptht 6442  exple1t 6546  crulem 6674  replimt 6700  bccl2t 6917  infmap2lem2 7530  qdensere 7701  iscms2lem4 7942  grpinveu 8014  grpinvf 8029  iporthcom 8316  eff1i 8683  norm1ex 9061  projlem13 9137  projlem31 9155  dfch2 9187  shmods 9300  shmod 9301  orthin 9308  chssoct 9357  spansncv 9537  adjvalvalt 9800  kbpjt 9819  lnopunilem1 9873  cnlnssadj 9951  strlem4 10119  strlem5 10120  hstrlem4 10127  hstrlem5 10128  dmdmdt 10165  mdslle1 10181  mdslle2 10182  mdslmd1lem1 10189  atcvatlem 10249  atcvat4 10261  mdsymlem3 10269  cayleylem3 10345  fine2 10411  1ded 10551  1cat 10572

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