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  885  nfalt  1624  alexim  1691  19.36-1  1719  ax11ev  1874  equs5or  1876  necon2bd  2458  necon2d  2459  necon1bbiddc  2463  necon2abiddc  2466  necon2bbiddc  2467  necon4idc  2469  necon4ddc  2472  necon1bddc  2477  spc2gv  2894  spc3gv  2896  mo2icl  2982  reupick  3488  prneimg  3852  invdisj  4076  trin  4192  exmidsssnc  4287  ordsucss  4596  eqbrrdva  4892  elreldm  4950  elres  5041  xp11m  5167  ssrnres  5171  opelf  5498  dffo4  5785  dftpos3  6414  tfr1onlemaccex  6500  tfrcllemaccex  6513  nnaordex  6682  swoer  6716  map0g  6843  mapsn  6845  nneneq  7026  fnfi  7111  prarloclemlo  7689  genprndl  7716  genprndu  7717  cauappcvgprlemladdrl  7852  caucvgprlemladdrl  7873  caucvgsrlemoffres  7995  caucvgsr  7997  nntopi  8089  letr  8237  reapcotr  8753  apcotr  8762  mulext1  8767  lt2msq  9041  nneoor  9557  xrletr  10012  icoshft  10194  swrdccatin2  11269  caucvgre  11500  absext  11582  rexico  11740  summodc  11902  gcdeq0  12506  intopsn  13408  znleval  14625  tgcn  14890  cnptoprest  14921  metequiv2  15178  bj-nnsn  16121  bj-inf2vnlem2  16358