Theorem syl5bi 183

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 135	. 2 ⊢ (φ → (ψ → χ))
3		syl5bi.2	. 2 ⊢ (θ → ψ)
4	2, 3	syl5 22	1 ⊢ (φ → (θ → χ))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  gencl 1365  a4sbc 1444  hbsbcg 1445  ssnelpss 1751  prex 1892  opth 1898  sotric 2148  sotrieq 2149  nordeq 2218  ordtri3 2234  nsuceq0 2306  brelg 2458  optocl 2469  funimass1 2712  f1ocnvb 2812  tz6.12-2 2845  fniunfv 2860  cleqfv 2880  f1fv 2916  f1ocnvfv 2921  f1ocnvfvb 2922  tz7.48-1 2994  tz7.49 2997  oawordeulem 3156  oalimcl 3162  ectocl 3238  ecoptocl 3239  eceqopreq 3249  mapsn 3269  eqeng 3296  undom 3342  pw2en 3348  mapdom2 3389  isfinite2 3437  unfi 3441  suc11reg 3456  inf0 3457  inf3lem6 3469  scott0 3542  aceq5 3563  zornlem4 3606  zornlem5 3607  zornlem6 3608  carduni 3664  axrepndlem2 3739  axunnd 3742  axregnd 3750  mulcanpi 3821  indpi 3828  ltaddpq 3873  nsmallpq 3877  ltbtwnpq 3878  addclprlem1 3912  distrlem4pr 3924  ltaddpr2 3935  ltaprlem 3944  reclem3pr 3952  supsrlem2 4020  axrecex 4079  negeu 4124  receu 4215  divge0 4392  nnaddclt 4436  crulem 4528  lt0nnn0 4549  zmulclt 4596  zneo 4601  qnegclt 4643  om2uzlt 4654  om2uzran 4655  ruclem33 4917  ruclem35 4919  infmap2lem2 4952  projlem13 5205  projlem31 5223  dfch2 5254  pjoml 5271  shmods 5363  shmod 5364  orthin 5371  h1dn0 5457  spansneleqi 5474  spansncv 5542  stm1 5684  strlem4 5695  strlem5 5696  mdbr2 5728  dmdbr 5731  atcvatlem 5770  atcvat4 5775  mdsymlem3 5778  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org