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  939  oplem1  978  3impexpbicom  1459  hband  1513  hb3and  1514  nfand  1592  nfimd  1609  equsexd  1753  euim  2123  mopick2  2138  2moswapdc  2145  necon3bd  2420  necon3d  2421  necon2ad  2434  necon1abiddc  2439  ralrimd  2585  rspcimedv  2880  2reuswapdc  2978  ra5  3088  difin  3411  r19.2m  3548  r19.2mOLD  3549  tpid3g  3749  sssnm  3797  ssiun  3971  ssiun2  3972  disjnim  4037  exmidsssnc  4251  sotricim  4374  sotritrieq  4376  tron  4433  ordsucss  4556  ordunisuc2r  4566  ordpwsucss  4619  dmcosseq  4955  relssres  5002  trin2  5079  ssrnres  5130  fnun  5387  f1oun  5549  ssimaex  5647  chfnrn  5698  dffo4  5735  dffo5  5736  isoselem  5896  fnoprabg  6053  poxp  6325  issmo2  6382  smores  6385  tfr0dm  6415  tfrlemibxssdm  6420  tfr1onlembxssdm  6436  tfrcllembxssdm  6449  swoer  6655  qsss  6688  findcard  6992  findcard2  6993  findcard2s  6994  supmoti  7102  ctmlemr  7217  ctm  7218  pm54.43  7305  indpi  7462  recexprlemm  7744  recexprlemloc  7751  recexprlem1ssl  7753  recexprlem1ssu  7754  recexprlemss1l  7755  recexprlemss1u  7756  zmulcl  9433  indstr  9721  eluzdc  9738  icoshft  10119  fzouzsplit  10310  seqf1oglem1  10671  seqf1oglem2  10672  hashunlem  10956  modfsummod  11813  dvds2lem  12158  oddnn02np1  12235  dfgcd2  12379  sqrt2irr  12528  ennnfonelemhom  12830  omctfn  12858  ptex  13140  kerf1ghm  13654  rmodislmodlem  14156  distop  14601  epttop  14606  restdis  14700  cnrest2  14752  cnptopresti  14754  uptx  14790  txcn  14791  logbgcd1irr  15483  gausslemma2dlem1a  15579  2sqlem10  15646  decidr  15806  bj-charfunbi  15821  bj-omssind  15945  bj-om  15947  bj-inf2vnlem3  15982  bj-inf2vnlem4  15983