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  892  nfalt  1631  alexim  1698  19.36-1  1725  ax11ev  1881  equs5or  1883  necon2bd  2478  necon2d  2479  necon1bbiddc  2483  necon2abiddc  2486  necon2bbiddc  2487  necon4idc  2489  necon4ddc  2492  necon1bddc  2497  spc2gv  2916  spc3gv  2918  mo2icl  3005  reupick  3517  prneimg  3897  invdisj  4121  trin  4237  exmidsssnc  4338  ordsucss  4649  eqbrrdva  4948  elreldm  5006  elres  5097  xp11m  5224  ssrnres  5228  opelf  5558  dffo4  5850  dftpos3  6527  tfr1onlemaccex  6613  tfrcllemaccex  6626  nnaordex  6795  swoer  6829  map0g  6963  mapsn  6966  nneneq  7152  fnfi  7244  prarloclemlo  7855  genprndl  7882  genprndu  7883  cauappcvgprlemladdrl  8018  caucvgprlemladdrl  8039  caucvgsrlemoffres  8161  caucvgsr  8163  nntopi  8255  letr  8402  reapcotr  8920  apcotr  8929  mulext1  8934  lt2msq  9210  nneoor  9731  xrletr  10193  icoshft  10375  hashf1  11270  swrdccatin2  11484  caucvgre  11730  absext  11812  rexico  11970  summodc  12133  gcdeq0  12737  intopsn  13670  znleval  14971  tgcn  15292  cnptoprest  15323  metequiv2  15580  bj-nnsn  16744  bj-inf2vnlem2  16980