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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used 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  3899  invdisj  4123  trin  4239  exmidsssnc  4340  ordsucss  4651  eqbrrdva  4950  elreldm  5008  elres  5099  xp11m  5226  ssrnres  5230  opelf  5560  dffo4  5856  dftpos3  6533  tfr1onlemaccex  6619  tfrcllemaccex  6632  nnaordex  6801  swoer  6835  map0g  6969  mapsn  6972  nneneq  7158  fnfi  7250  prarloclemlo  7861  genprndl  7888  genprndu  7889  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  caucvgsrlemoffres  8167  caucvgsr  8169  nntopi  8261  letr  8408  reapcotr  8927  apcotr  8936  mulext1  8941  lt2msq  9217  nneoor  9750  xrletr  10212  icoshft  10394  hashf1  11289  swrdccatin2  11503  caucvgre  11749  absext  11831  rexico  11989  summodc  12152  gcdeq0  12756  intopsn  13689  znleval  14990  tgcn  15311  cnptoprest  15342  metequiv2  15599  bj-nnsn  16773  bj-inf2vnlem2  17009