Theorem syl6ib 161

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3g  204  exp4a  366  con2biddc  880  nfalt  1576  alexim  1643  19.36-1  1671  ax11ev  1826  equs5or  1828  necon2bd  2403  necon2d  2404  necon1bbiddc  2408  necon2abiddc  2411  necon2bbiddc  2412  necon4idc  2414  necon4ddc  2417  necon1bddc  2422  spc2gv  2826  spc3gv  2828  mo2icl  2914  reupick  3417  prneimg  3770  invdisj  3992  trin  4106  exmidsssnc  4198  ordsucss  4497  eqbrrdva  4790  elreldm  4846  elres  4936  xp11m  5059  ssrnres  5063  opelf  5379  dffo4  5656  dftpos3  6253  tfr1onlemaccex  6339  tfrcllemaccex  6352  nnaordex  6519  swoer  6553  map0g  6678  mapsn  6680  nneneq  6847  fnfi  6926  prarloclemlo  7468  genprndl  7495  genprndu  7496  cauappcvgprlemladdrl  7631  caucvgprlemladdrl  7652  caucvgsrlemoffres  7774  caucvgsr  7776  nntopi  7868  letr  8014  reapcotr  8529  apcotr  8538  mulext1  8543  lt2msq  8814  nneoor  9326  xrletr  9777  icoshft  9959  caucvgre  10956  absext  11038  rexico  11196  summodc  11357  gcdeq0  11943  intopsn  12650  tgcn  13259  cnptoprest  13290  metequiv2  13547  bj-nnsn  14025  bj-inf2vnlem2  14263