Theorem syl6ib 150

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

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	biimpi 113	. 2 ⊢ (χ → θ)
4	1, 3	syl6 29	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3imtr3g  193  exp4a  348  con2biddc  762  nfalt  1448  alexim  1514  19.36-1  1541  ax11ev  1687  equs5or  1689  necon2bd  2237  necon2d  2238  necon1bbiddc  2242  necon2abiddc  2245  necon2bbiddc  2246  necon4idc  2248  necon4ddc  2251  necon1bddc  2256  spc2gv  2616  spc3gv  2618  mo2icl  2693  eqsbc3r  2792  reupick  3194  prneimg  3515  invdisj  3729  trin  3834  ordsucss  4176  eqbrrdva  4428  elreldm  4483  elres  4569  xp11m  4682  ssrnres  4686  opelf  4983  dffo4  5236  dftpos3  5795  frec0g  5898  nnaordex  6007  swoer  6041  prarloclemlo  6342  genprndl  6370  genprndu  6371  letr  6693  bj-inf2vnlem2  7328