Theorem syl5bi 206

Description: A mixed syllogism inference.

Hypotheses

Ref	Expression
syl5bi.1	⊢ (φ → (ψ ↔ χ))
syl5bi.2	⊢ (θ → ψ)

Assertion

Ref	Expression
syl5bi	⊢ (φ → (θ → χ))

Proof of Theorem syl5bi

Step	Hyp	Ref	Expression
1		syl5bi.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	biimpd 151	. 2 ⊢ (φ → (ψ → χ))
3		syl5bi.2	. 2 ⊢ (θ → ψ)
4	2, 3	syl5 21	1 ⊢ (φ → (θ → χ))

Syntax hints:   → wi 3   ↔ wb 144

This theorem is referenced by:  syl5cbi 207  ax11indalem 1407  ax11inda2ALT 1408  gencl 1874  a4sbc 1990  hbsbc1g 1993  ssnelpss 2383  prex 2857  opth 2863  sotrieq 2940  ordtri3 3011  brelg 3307  optocl 3321  xpexr 3564  relcnvexb 3626  funimass1 3677  f1ocnvb 3810  tz6.12-2 3850  fnrnfv 3870  eqfnfv 3909  eqfnfv2 3911  fconst5 3962  funiunfv 3980  dff13 3988  f1ocnvfv 3994  f1ocnvfvb 3995  oawordeulem 4324  oalimcl 4330  odi 4346  eceqopreq 4454  undom 4579  mapdom2 4641  isfinite2 4692  unfi 4697  inf0 4751  rankr1b 4845  rankxplim2 4859  scott0 4863  aceq5 4886  zorn2lem5 4938  zorn2lem6 4939  carduni 5008  axrepndlem2 5099  axunnd 5102  axregnd 5110  mulcanpi 5181  indpi 5188  ltaddpq 5233  nsmallpq 5237  ltbtwnpq 5238  addclprlem1 5272  ltaddpr2 5295  ltaprlem 5304  reclem3pr 5312  supsrlem2 5380  negeui 5509  xrltne 5719  receui 5853  nnaddcl 6085  nndivtr 6106  xrsupss 6246  xrinfmss 6247  zmulcl 6348  zeo 6370  zneo 6371  qnegcl 6409  modadd1 6477  modmul1 6478  uz11 6559  fzopth 6632  om2uzlti 6661  exple1 6804  crulem 6937  replim 6962  cj11 7031  bccl2 7174  infmap2lem2 7792  qdensere 7961  iscms2lem4 8203  grpinveu 8281  grpinvf 8297  iporthcom 8623  eff1i 9016  norm1exi 9398  projlem13 9474  projlem31 9492  dfch2 9525  shmodsi 9638  shmodi 9639  orthin 9646  chssoc 9695  spansncvi 9875  adjvalval 10141  kbpj 10160  lnopunilem1 10214  cnlnssadj 10292  strlem4 10462  strlem5 10463  hstrlem4 10470  hstrlem5 10471  dmdmd 10508  mdslle1i 10525  mdslle2i 10526  mdslmd1lem1 10533  atcvatlem 10594  atcvat4i 10606  mdsymlem3 10614  cayleylem3 10696  fine2 10850  fillsb 11073  1ded 11192  1cat 11213  ordtypelem7 11433  fcluscf 11724  filnetlem5 11767  gapmlem 11783  elpreima 11792  uzp1 11863  absz 11868  negmod0 11872  totbndbnd 12000

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 145

Copyright terms: Public domain