Theorem syl6ib 159

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 118	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr3g  202  exp4a  358  con2biddc  808  nfalt  1511  alexim  1577  19.36-1  1604  ax11ev  1750  equs5or  1752  necon2bd  2304  necon2d  2305  necon1bbiddc  2309  necon2abiddc  2312  necon2bbiddc  2313  necon4idc  2315  necon4ddc  2318  necon1bddc  2323  spc2gv  2689  spc3gv  2691  mo2icl  2772  reupick  3255  prneimg  3574  invdisj  3788  trin  3893  ordsucss  4256  eqbrrdva  4533  elreldm  4588  elres  4674  xp11m  4789  ssrnres  4793  opelf  5093  dffo4  5347  dftpos3  5911  tfr1onlemaccex  5997  tfrcllemaccex  6010  nnaordex  6166  swoer  6200  nneneq  6392  fnfi  6446  prarloclemlo  6746  genprndl  6773  genprndu  6774  cauappcvgprlemladdrl  6909  caucvgprlemladdrl  6930  caucvgsrlemoffres  7038  caucvgsr  7040  nntopi  7122  letr  7261  reapcotr  7765  apcotr  7774  mulext1  7779  lt2msq  8031  nneoor  8530  xrletr  8954  icoshft  9088  caucvgre  10005  absext  10087  rexico  10245  gcdeq0  10512  bj-inf2vnlem2  10924