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  4288  ordsucss  4597  eqbrrdva  4895  elreldm  4953  elres  5044  xp11m  5170  ssrnres  5174  opelf  5501  dffo4  5788  dftpos3  6419  tfr1onlemaccex  6505  tfrcllemaccex  6518  nnaordex  6687  swoer  6721  map0g  6848  mapsn  6850  nneneq  7031  fnfi  7119  prarloclemlo  7697  genprndl  7724  genprndu  7725  cauappcvgprlemladdrl  7860  caucvgprlemladdrl  7881  caucvgsrlemoffres  8003  caucvgsr  8005  nntopi  8097  letr  8245  reapcotr  8761  apcotr  8770  mulext1  8775  lt2msq  9049  nneoor  9565  xrletr  10021  icoshft  10203  swrdccatin2  11282  caucvgre  11513  absext  11595  rexico  11753  summodc  11915  gcdeq0  12519  intopsn  13421  znleval  14638  tgcn  14903  cnptoprest  14934  metequiv2  15191  bj-nnsn  16206  bj-inf2vnlem2  16443