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  887  nfalt  1626  alexim  1693  19.36-1  1720  ax11ev  1875  equs5or  1877  necon2bd  2459  necon2d  2460  necon1bbiddc  2464  necon2abiddc  2467  necon2bbiddc  2468  necon4idc  2470  necon4ddc  2473  necon1bddc  2478  spc2gv  2896  spc3gv  2898  mo2icl  2984  reupick  3490  prneimg  3858  invdisj  4082  trin  4198  exmidsssnc  4295  ordsucss  4604  eqbrrdva  4902  elreldm  4960  elres  5051  xp11m  5177  ssrnres  5181  opelf  5509  dffo4  5798  dftpos3  6433  tfr1onlemaccex  6519  tfrcllemaccex  6532  nnaordex  6701  swoer  6735  map0g  6862  mapsn  6864  nneneq  7048  fnfi  7140  prarloclemlo  7719  genprndl  7746  genprndu  7747  cauappcvgprlemladdrl  7882  caucvgprlemladdrl  7903  caucvgsrlemoffres  8025  caucvgsr  8027  nntopi  8119  letr  8267  reapcotr  8783  apcotr  8792  mulext1  8797  lt2msq  9071  nneoor  9587  xrletr  10048  icoshft  10230  swrdccatin2  11319  caucvgre  11564  absext  11646  rexico  11804  summodc  11967  gcdeq0  12571  intopsn  13473  znleval  14691  tgcn  14961  cnptoprest  14992  metequiv2  15249  bj-nnsn  16390  bj-inf2vnlem2  16626