Theorem imbitrrdi 162

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbitrrdi.1	⊢ (𝜑 → (𝜓 → 𝜒))
imbitrrdi.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
imbitrrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem imbitrrdi

Step	Hyp	Ref	Expression
1		imbitrrdi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		imbitrrdi.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	biimpri 133	. 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  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr4g  205  imp4a  349  dcbi  941  oplem1  980  3impexpbicom  1461  hband  1515  hb3and  1516  nfand  1594  nfimd  1611  equsexd  1755  euim  2126  mopick2  2141  2moswapdc  2148  necon3bd  2423  necon3d  2424  necon2ad  2437  necon1abiddc  2442  ralrimd  2588  rspcimedv  2889  2reuswapdc  2987  ra5  3098  difin  3421  r19.2m  3558  r19.2mOLD  3559  tpid3g  3761  sssnm  3811  ssiun  3986  ssiun2  3987  disjnim  4052  exmidsssnc  4266  sotricim  4391  sotritrieq  4393  tron  4450  ordsucss  4573  ordunisuc2r  4583  ordpwsucss  4636  dmcosseq  4972  relssres  5019  trin2  5096  ssrnres  5147  fnun  5405  f1oun  5568  ssimaex  5668  chfnrn  5719  dffo4  5756  dffo5  5757  isoselem  5917  fnoprabg  6076  poxp  6348  issmo2  6405  smores  6408  tfr0dm  6438  tfrlemibxssdm  6443  tfr1onlembxssdm  6459  tfrcllembxssdm  6472  swoer  6678  qsss  6711  findcard  7018  findcard2  7019  findcard2s  7020  supmoti  7128  ctmlemr  7243  ctm  7244  pm54.43  7331  indpi  7497  recexprlemm  7779  recexprlemloc  7786  recexprlem1ssl  7788  recexprlem1ssu  7789  recexprlemss1l  7790  recexprlemss1u  7791  zmulcl  9468  indstr  9756  eluzdc  9773  icoshft  10154  fzouzsplit  10345  seqf1oglem1  10708  seqf1oglem2  10709  hashunlem  10993  modfsummod  11935  dvds2lem  12280  oddnn02np1  12357  dfgcd2  12501  sqrt2irr  12650  ennnfonelemhom  12952  omctfn  12980  ptex  13263  kerf1ghm  13777  rmodislmodlem  14279  distop  14724  epttop  14729  restdis  14823  cnrest2  14875  cnptopresti  14877  uptx  14913  txcn  14914  logbgcd1irr  15606  gausslemma2dlem1a  15702  2sqlem10  15769  decidr  16070  bj-charfunbi  16084  bj-omssind  16208  bj-om  16210  bj-inf2vnlem3  16245  bj-inf2vnlem4  16246