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  1592  alexim  1659  19.36-1  1687  ax11ev  1842  equs5or  1844  necon2bd  2425  necon2d  2426  necon1bbiddc  2430  necon2abiddc  2433  necon2bbiddc  2434  necon4idc  2436  necon4ddc  2439  necon1bddc  2444  spc2gv  2855  spc3gv  2857  mo2icl  2943  reupick  3448  prneimg  3805  invdisj  4028  trin  4142  exmidsssnc  4237  ordsucss  4541  eqbrrdva  4837  elreldm  4893  elres  4983  xp11m  5109  ssrnres  5113  opelf  5432  dffo4  5713  dftpos3  6329  tfr1onlemaccex  6415  tfrcllemaccex  6428  nnaordex  6595  swoer  6629  map0g  6756  mapsn  6758  nneneq  6927  fnfi  7011  prarloclemlo  7580  genprndl  7607  genprndu  7608  cauappcvgprlemladdrl  7743  caucvgprlemladdrl  7764  caucvgsrlemoffres  7886  caucvgsr  7888  nntopi  7980  letr  8128  reapcotr  8644  apcotr  8653  mulext1  8658  lt2msq  8932  nneoor  9447  xrletr  9902  icoshft  10084  caucvgre  11165  absext  11247  rexico  11405  summodc  11567  gcdeq0  12171  intopsn  13071  znleval  14287  tgcn  14552  cnptoprest  14583  metequiv2  14840  bj-nnsn  15487  bj-inf2vnlem2  15725