Theorem syl6ib 160

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3g  203  exp4a  363  con2biddc  865  nfalt  1557  alexim  1624  19.36-1  1651  ax11ev  1800  equs5or  1802  necon2bd  2364  necon2d  2365  necon1bbiddc  2369  necon2abiddc  2372  necon2bbiddc  2373  necon4idc  2375  necon4ddc  2378  necon1bddc  2383  spc2gv  2771  spc3gv  2773  mo2icl  2858  reupick  3355  prneimg  3696  invdisj  3918  trin  4031  exmidsssnc  4121  ordsucss  4415  eqbrrdva  4704  elreldm  4760  elres  4850  xp11m  4972  ssrnres  4976  opelf  5289  dffo4  5561  dftpos3  6152  tfr1onlemaccex  6238  tfrcllemaccex  6251  nnaordex  6416  swoer  6450  map0g  6575  mapsn  6577  nneneq  6744  fnfi  6818  prarloclemlo  7295  genprndl  7322  genprndu  7323  cauappcvgprlemladdrl  7458  caucvgprlemladdrl  7479  caucvgsrlemoffres  7601  caucvgsr  7603  nntopi  7695  letr  7840  reapcotr  8353  apcotr  8362  mulext1  8367  cnstab  8400  lt2msq  8637  nneoor  9146  xrletr  9584  icoshft  9766  caucvgre  10746  absext  10828  rexico  10986  summodc  11145  gcdeq0  11654  tgcn  12366  cnptoprest  12397  metequiv2  12654  bj-nnsn  12934  bj-inf2vnlem2  13158