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  880  nfalt  1578  alexim  1645  19.36-1  1673  ax11ev  1828  equs5or  1830  necon2bd  2405  necon2d  2406  necon1bbiddc  2410  necon2abiddc  2413  necon2bbiddc  2414  necon4idc  2416  necon4ddc  2419  necon1bddc  2424  spc2gv  2829  spc3gv  2831  mo2icl  2917  reupick  3420  prneimg  3775  invdisj  3998  trin  4112  exmidsssnc  4204  ordsucss  4504  eqbrrdva  4798  elreldm  4854  elres  4944  xp11m  5068  ssrnres  5072  opelf  5388  dffo4  5665  dftpos3  6263  tfr1onlemaccex  6349  tfrcllemaccex  6362  nnaordex  6529  swoer  6563  map0g  6688  mapsn  6690  nneneq  6857  fnfi  6936  prarloclemlo  7493  genprndl  7520  genprndu  7521  cauappcvgprlemladdrl  7656  caucvgprlemladdrl  7677  caucvgsrlemoffres  7799  caucvgsr  7801  nntopi  7893  letr  8040  reapcotr  8555  apcotr  8564  mulext1  8569  lt2msq  8843  nneoor  9355  xrletr  9808  icoshft  9990  caucvgre  10990  absext  11072  rexico  11230  summodc  11391  gcdeq0  11978  intopsn  12786  tgcn  13711  cnptoprest  13742  metequiv2  13999  bj-nnsn  14488  bj-inf2vnlem2  14726