Theorem imbitrdi 161

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbitrdi.1	⊢ (𝜑 → (𝜓 → 𝜒))
imbitrdi.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
imbitrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem imbitrdi

Step	Hyp	Ref	Expression
1		imbitrdi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		imbitrdi.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  881  nfalt  1589  alexim  1656  19.36-1  1684  ax11ev  1839  equs5or  1841  necon2bd  2422  necon2d  2423  necon1bbiddc  2427  necon2abiddc  2430  necon2bbiddc  2431  necon4idc  2433  necon4ddc  2436  necon1bddc  2441  spc2gv  2852  spc3gv  2854  mo2icl  2940  reupick  3444  prneimg  3801  invdisj  4024  trin  4138  exmidsssnc  4233  ordsucss  4537  eqbrrdva  4833  elreldm  4889  elres  4979  xp11m  5105  ssrnres  5109  opelf  5426  dffo4  5707  dftpos3  6317  tfr1onlemaccex  6403  tfrcllemaccex  6416  nnaordex  6583  swoer  6617  map0g  6744  mapsn  6746  nneneq  6915  fnfi  6997  prarloclemlo  7556  genprndl  7583  genprndu  7584  cauappcvgprlemladdrl  7719  caucvgprlemladdrl  7740  caucvgsrlemoffres  7862  caucvgsr  7864  nntopi  7956  letr  8104  reapcotr  8619  apcotr  8628  mulext1  8633  lt2msq  8907  nneoor  9422  xrletr  9877  icoshft  10059  caucvgre  11128  absext  11210  rexico  11368  summodc  11529  gcdeq0  12117  intopsn  12953  znleval  14152  tgcn  14387  cnptoprest  14418  metequiv2  14675  bj-nnsn  15295  bj-inf2vnlem2  15533