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  888  nfalt  1627  alexim  1694  19.36-1  1721  ax11ev  1877  equs5or  1879  necon2bd  2470  necon2d  2471  necon1bbiddc  2475  necon2abiddc  2478  necon2bbiddc  2479  necon4idc  2481  necon4ddc  2484  necon1bddc  2489  spc2gv  2907  spc3gv  2909  mo2icl  2995  reupick  3504  prneimg  3877  invdisj  4101  trin  4217  exmidsssnc  4315  ordsucss  4625  eqbrrdva  4924  elreldm  4982  elres  5073  xp11m  5200  ssrnres  5204  opelf  5534  dffo4  5824  dftpos3  6492  tfr1onlemaccex  6578  tfrcllemaccex  6591  nnaordex  6760  swoer  6794  map0g  6921  mapsn  6924  nneneq  7110  fnfi  7202  prarloclemlo  7805  genprndl  7832  genprndu  7833  cauappcvgprlemladdrl  7968  caucvgprlemladdrl  7989  caucvgsrlemoffres  8111  caucvgsr  8113  nntopi  8205  letr  8352  reapcotr  8868  apcotr  8877  mulext1  8882  lt2msq  9156  nneoor  9676  xrletr  10137  icoshft  10319  swrdccatin2  11414  caucvgre  11659  absext  11741  rexico  11899  summodc  12062  gcdeq0  12666  intopsn  13569  znleval  14788  tgcn  15060  cnptoprest  15091  metequiv2  15348  bj-nnsn  16492  bj-inf2vnlem2  16728