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  2895  spc3gv  2897  mo2icl  2983  reupick  3489  prneimg  3855  invdisj  4079  trin  4195  exmidsssnc  4291  ordsucss  4600  eqbrrdva  4898  elreldm  4956  elres  5047  xp11m  5173  ssrnres  5177  opelf  5504  dffo4  5791  dftpos3  6423  tfr1onlemaccex  6509  tfrcllemaccex  6522  nnaordex  6691  swoer  6725  map0g  6852  mapsn  6854  nneneq  7038  fnfi  7129  prarloclemlo  7707  genprndl  7734  genprndu  7735  cauappcvgprlemladdrl  7870  caucvgprlemladdrl  7891  caucvgsrlemoffres  8013  caucvgsr  8015  nntopi  8107  letr  8255  reapcotr  8771  apcotr  8780  mulext1  8785  lt2msq  9059  nneoor  9575  xrletr  10036  icoshft  10218  swrdccatin2  11303  caucvgre  11535  absext  11617  rexico  11775  summodc  11937  gcdeq0  12541  intopsn  13443  znleval  14660  tgcn  14925  cnptoprest  14956  metequiv2  15213  bj-nnsn  16279  bj-inf2vnlem2  16516