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  6477  genprndl  6504  genprndu  6505  cauappcvgprlemladdrl  6629  caucvgprlemladdrl  6649  letr  6898  reapcotr  7382  apcotr  7391  mulext1  7396  lt2msq  7633  nneoor  8116  xrletr  8494  icoshft  8628  bj-inf2vnlem2  9431