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  938  oplem1  977  3impexpbicom  1449  hband  1503  hb3and  1504  nfand  1582  nfimd  1599  equsexd  1743  euim  2113  mopick2  2128  2moswapdc  2135  necon3bd  2410  necon3d  2411  necon2ad  2424  necon1abiddc  2429  ralrimd  2575  rspcimedv  2870  2reuswapdc  2968  ra5  3078  difin  3401  r19.2m  3538  r19.2mOLD  3539  tpid3g  3738  sssnm  3785  ssiun  3959  ssiun2  3960  disjnim  4025  exmidsssnc  4237  sotricim  4359  sotritrieq  4361  tron  4418  ordsucss  4541  ordunisuc2r  4551  ordpwsucss  4604  dmcosseq  4938  relssres  4985  trin2  5062  ssrnres  5113  fnun  5367  f1oun  5527  ssimaex  5625  chfnrn  5676  dffo4  5713  dffo5  5714  isoselem  5870  fnoprabg  6027  poxp  6299  issmo2  6356  smores  6359  tfr0dm  6389  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  swoer  6629  qsss  6662  findcard  6958  findcard2  6959  findcard2s  6960  supmoti  7068  ctmlemr  7183  ctm  7184  pm54.43  7271  indpi  7428  recexprlemm  7710  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1l  7721  recexprlemss1u  7722  zmulcl  9398  indstr  9686  eluzdc  9703  icoshft  10084  fzouzsplit  10274  seqf1oglem1  10630  seqf1oglem2  10631  hashunlem  10915  modfsummod  11642  dvds2lem  11987  oddnn02np1  12064  dfgcd2  12208  sqrt2irr  12357  ennnfonelemhom  12659  omctfn  12687  ptex  12968  kerf1ghm  13482  rmodislmodlem  13984  distop  14429  epttop  14434  restdis  14528  cnrest2  14580  cnptopresti  14582  uptx  14618  txcn  14619  logbgcd1irr  15311  gausslemma2dlem1a  15407  2sqlem10  15474  decidr  15550  bj-charfunbi  15565  bj-omssind  15689  bj-om  15691  bj-inf2vnlem3  15726  bj-inf2vnlem4  15727