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  773  nfalt  1467  alexim  1533  19.36-1  1560  ax11ev  1706  equs5or  1708  necon2bd  2257  necon2d  2258  necon1bbiddc  2262  necon2abiddc  2265  necon2bbiddc  2266  necon4idc  2268  necon4ddc  2271  necon1bddc  2276  spc2gv  2637  spc3gv  2639  mo2icl  2714  eqsbc3r  2813  reupick  3215  prneimg  3536  invdisj  3750  trin  3855  ordsucss  4196  eqbrrdva  4448  elreldm  4503  elres  4589  xp11m  4702  ssrnres  4706  opelf  5005  dffo4  5258  dftpos3  5818  tfr0  5878  nnaordex  6036  swoer  6070  prarloclemlo  6476  genprndl  6503  genprndu  6504  cauappcvgprlemladdrl  6628  letr  6878  reapcotr  7362  apcotr  7371  mulext1  7376  lt2msq  7613  nneoor  8096  xrletr  8474  icoshft  8608  bj-inf2vnlem2  9401