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  4241  exmidsssnc  4342  ordsucss  4653  eqbrrdva  4952  elreldm  5010  elres  5101  xp11m  5229  ssrnres  5233  opelf  5563  dffo4  5859  dftpos3  6537  tfr1onlemaccex  6623  tfrcllemaccex  6636  nnaordex  6805  swoer  6839  map0g  6973  mapsn  6977  nneneq  7163  fnfi  7255  prarloclemlo  7868  genprndl  7895  genprndu  7896  cauappcvgprlemladdrl  8031  caucvgprlemladdrl  8052  caucvgsrlemoffres  8174  caucvgsr  8176  nntopi  8268  letr  8415  reapcotr  8935  apcotr  8944  mulext1  8949  lt2msq  9225  nneoor  9760  xrletr  10228  icoshft  10410  hashf1  11310  swrdccatin2  11524  caucvgre  11770  absext  11852  rexico  12011  summodc  12176  gcdeq0  12780  intopsn  13747  znleval  15098  tgcn  15446  cnptoprest  15477  metequiv2  15734  ppiqeq0  16292  bposlem6  16328  bj-nnsn  16978  bj-inf2vnlem2  17214