Theorem syl6bir 188

Description: A mixed syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
syl6bir	⊢ (φ → (ψ → θ))

Proof of Theorem syl6bir

Step	Hyp	Ref	Expression
1		syl6bir.1	. . 3 ⊢ (φ → (χ ↔ ψ))
2	1	biimprd 136	. 2 ⊢ (φ → (ψ → χ))
3		syl6bir.2	. 2 ⊢ (χ → θ)
4	2, 3	syl6 23	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  19.33b 771  reuuni1 1955  onint 2261  ordsuc 2318  findsg 2398  tfindsg 2402  fneu 2728  fnun 2730  zfrep6 2744  tz6.12i 2847  tfrlem9 2957  tfr3 2964  ndmoprg 3057  pssnn 3428  aceq6b 3565  carddom 3642  axextnd 3737  indpi 3828  ltexpq 3874  ltexpq2 3875  nsmallpq 3877  ltbtwnpq 3878  ltaddpr2 3935  ltexpri 3943  reclem2pr 3951  suppsr2 4017  axrnegex 4080  axrrecex 4081  cru 4529  nn0ind 4612  h1de2ctlem 5460  pjclem4a 5652  pj3lem1 5658  chrelat2 5758  sumdmdi 5785

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