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  364  con2biddc  870  nfalt  1565  alexim  1632  19.36-1  1660  ax11ev  1815  equs5or  1817  necon2bd  2392  necon2d  2393  necon1bbiddc  2397  necon2abiddc  2400  necon2bbiddc  2401  necon4idc  2403  necon4ddc  2406  necon1bddc  2411  spc2gv  2812  spc3gv  2814  mo2icl  2900  reupick  3401  prneimg  3748  invdisj  3970  trin  4084  exmidsssnc  4176  ordsucss  4475  eqbrrdva  4768  elreldm  4824  elres  4914  xp11m  5036  ssrnres  5040  opelf  5353  dffo4  5627  dftpos3  6221  tfr1onlemaccex  6307  tfrcllemaccex  6320  nnaordex  6486  swoer  6520  map0g  6645  mapsn  6647  nneneq  6814  fnfi  6893  prarloclemlo  7426  genprndl  7453  genprndu  7454  cauappcvgprlemladdrl  7589  caucvgprlemladdrl  7610  caucvgsrlemoffres  7732  caucvgsr  7734  nntopi  7826  letr  7972  reapcotr  8487  apcotr  8496  mulext1  8501  lt2msq  8772  nneoor  9284  xrletr  9735  icoshft  9917  caucvgre  10909  absext  10991  rexico  11149  summodc  11310  gcdeq0  11895  tgcn  12749  cnptoprest  12780  metequiv2  13037  bj-nnsn  13451  bj-inf2vnlem2  13688