Theorem syl6ib 185

Description: A mixed syllogism inference from a nested implication and a biconditional.

Hypotheses

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

Assertion

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

Proof of Theorem syl6ib

Step	Hyp	Ref	Expression
1		syl6ib.1	. 2 ⊢ (φ → (ψ → χ))
2		syl6ib.2	. . 3 ⊢ (χ ↔ θ)
3	2	biimp 133	. 2 ⊢ (χ → θ)
4	1, 3	syl6 23	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  exp4a 295  pm5.18 497  19.29 752  cbvexd 978  ax15 1006  2eu3 1069  reupick 1578  pwssun 1917  trin 2051  supmo 2156  supnub 2162  efrirr 2180  wefrc 2195  onfr 2237  suc11 2341  relss 2480  elreldm 2554  iss 2599  resfunexg 2717  opelf 2762  mapsn 3269  en2d 3303  nneneq 3408  unblem1 3431  suc11reg 3456  inf3lem2 3465  trcl 3489  tz9.13 3507  aceq5lem5 3562  entri 3645  unxpdomlem 3649  carduniima 3695  cardinfima 3696  distrlem2pr 3922  ltapr 3945  suppsrlem 4015  suppsr2 4017  suprelem 4053  divge0 4392  sup2 4510  nnunb 4520  elnn0nn 4593  indstr 4611  uzwo3lem1 4614  nneo 4719  h1dn0 5457  osumlem5 5534  cvnbtwn2t 5719  cvnbtwn3t 5720  cvnbtwn4t 5721  dmdbr2 5733  atcvat 5771  mdsymlem4 5779  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