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  881  nfalt  1589  alexim  1656  19.36-1  1684  ax11ev  1839  equs5or  1841  necon2bd  2422  necon2d  2423  necon1bbiddc  2427  necon2abiddc  2430  necon2bbiddc  2431  necon4idc  2433  necon4ddc  2436  necon1bddc  2441  spc2gv  2851  spc3gv  2853  mo2icl  2939  reupick  3443  prneimg  3800  invdisj  4023  trin  4137  exmidsssnc  4232  ordsucss  4536  eqbrrdva  4832  elreldm  4888  elres  4978  xp11m  5104  ssrnres  5108  opelf  5425  dffo4  5706  dftpos3  6315  tfr1onlemaccex  6401  tfrcllemaccex  6414  nnaordex  6581  swoer  6615  map0g  6742  mapsn  6744  nneneq  6913  fnfi  6995  prarloclemlo  7554  genprndl  7581  genprndu  7582  cauappcvgprlemladdrl  7717  caucvgprlemladdrl  7738  caucvgsrlemoffres  7860  caucvgsr  7862  nntopi  7954  letr  8102  reapcotr  8617  apcotr  8626  mulext1  8631  lt2msq  8905  nneoor  9419  xrletr  9874  icoshft  10056  caucvgre  11125  absext  11207  rexico  11365  summodc  11526  gcdeq0  12114  intopsn  12950  znleval  14141  tgcn  14376  cnptoprest  14407  metequiv2  14664  bj-nnsn  15225  bj-inf2vnlem2  15463