Theorem syl5bi 225

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 170	. 2 |- (ph -> (ps -> ch))
3		syl5bi.2	. 2 |- (th -> ps)
4	2, 3	syl5 20	1 |- (ph -> (th -> ch))

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

This theorem is referenced by:  syl5cbi 226  orbi1r 1282  ax11indalem 1759  ax11inda2ALT 1760  gencl 2318  a4sbc 2457  hbsbc1g 2461  ssnelpss 2937  uniintsn 3253  prex 3526  opth 3532  sotrieqOLD 3617  ordtri3 3697  ordtri3OLD 3698  brelg 4047  optocl 4061  xpexr 4352  relcnvexb 4426  funimass1 4491  fneu 4517  dmfex 4598  f1ocnvb 4653  tz6.12-2 4696  fnrnfv 4718  eqfnfv 4766  fconst5 4824  funiunfv 4842  dff13 4850  f1ocnvfv 4856  f1ocnvfvb 4857  oawordeulem 5236  oalimcl 5242  odi 5258  eceqopreq 5372  undom 5497  mapdom2 5588  isfinite2 5639  unfi 5644  ordtypelem7 5690  inf0 5712  rankr1b 5810  rankxplim2 5824  scott0 5847  aceq5 5902  zorn2lem5 5954  zorn2lem6 5955  carduni 6010  axrepndlem2 6097  axunnd 6100  axregnd 6108  mulcanpi 6179  indpi 6186  ltaddpq 6231  nsmallpq 6235  ltbtwnpq 6236  addclprlem1 6270  ltaddpr2 6293  ltaprlem 6302  reclem3pr 6310  supsrlem2 6378  negeui 6510  ssxr 6714  xrltne 6740  receui 6890  nnaddcl 7123  nndivtr 7144  xrsupss 7287  xrinfmss 7288  zmulcl 7389  zeo 7411  zneo 7412  qnegcl 7450  modadd1 7518  modmul1 7519  uz11 7601  fzopth 7674  om2uzlti 7709  exple1 7852  crulem 7986  replim 8011  cj11 8080  bccl2 8223  hashen 8233  infmap2lem2 8849  qdensere 9027  iscms2lem4 9270  grpinveu 9348  grpinvf 9364  gapmlem 9461  iporthcom 9708  eff1i 10098  elpreima 10161  dif1en 10172  fine2 10214  fillsb 10270  norm1exi 10755  projlem13 10831  projlem31 10849  dfch2 10882  shmodsi 10995  shmodi 10996  orthin 11003  chssoc 11052  spansncvi 11232  adjvalval 11498  kbpj 11517  lnopunilem1 11572  cnlnssadj 11650  strlem4 11826  strlem5 11827  hstrlem4 11834  hstrlem5 11835  dmdmd 11872  mdslle1i 11889  mdslle2i 11890  mdslmd1lem1 11897  atcvatlem 11957  atcvat4i 11969  mdsymlem3 11977  bnj149 13241  bnj1125 13430  cayleylem3 13643  eqreznegel 13654  divalglem8 13703  funpsstri 13835  frxp 13951  axfelem12 14042  svs3 14830  1ded 15085  1cat 15106  ordtypelem7OLD 15381  fcluscf 15612  filnetlem5 15644  findcard2 15745  uzp1 15785  absz 15797  negmod0 15801  totbndbnd 15944  grpeqdivid 16038  pcorev 16087  0ring 16175  prter3 16286  sbiota1 16399  xpexcnv 16436  strdif 16719  lubid 16807  opcon3b 16923  ps-1 17078  grpinveuNEW 17123  paddcl 17303

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 164

Copyright terms: Public domain