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  884  nfalt  1604  alexim  1671  19.36-1  1699  ax11ev  1854  equs5or  1856  necon2bd  2438  necon2d  2439  necon1bbiddc  2443  necon2abiddc  2446  necon2bbiddc  2447  necon4idc  2449  necon4ddc  2452  necon1bddc  2457  spc2gv  2874  spc3gv  2876  mo2icl  2962  reupick  3468  prneimg  3831  invdisj  4055  trin  4171  exmidsssnc  4266  ordsucss  4573  eqbrrdva  4869  elreldm  4926  elres  5017  xp11m  5143  ssrnres  5147  opelf  5472  dffo4  5756  dftpos3  6378  tfr1onlemaccex  6464  tfrcllemaccex  6477  nnaordex  6644  swoer  6678  map0g  6805  mapsn  6807  nneneq  6986  fnfi  7071  prarloclemlo  7649  genprndl  7676  genprndu  7677  cauappcvgprlemladdrl  7812  caucvgprlemladdrl  7833  caucvgsrlemoffres  7955  caucvgsr  7957  nntopi  8049  letr  8197  reapcotr  8713  apcotr  8722  mulext1  8727  lt2msq  9001  nneoor  9517  xrletr  9972  icoshft  10154  swrdccatin2  11227  caucvgre  11458  absext  11540  rexico  11698  summodc  11860  gcdeq0  12464  intopsn  13366  znleval  14582  tgcn  14847  cnptoprest  14878  metequiv2  15135  bj-nnsn  16007  bj-inf2vnlem2  16244