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  942  oplem1  981  3impexpbicom  1481  hband  1535  hb3and  1536  nfand  1614  nfimd  1631  equsexd  1775  euim  2146  mopick2  2161  2moswapdc  2168  necon3bd  2443  necon3d  2444  necon2ad  2457  necon1abiddc  2462  ralrimd  2608  rspcimedv  2909  2reuswapdc  3007  ra5  3118  difin  3441  r19.2m  3578  r19.2mOLD  3579  tpid3g  3782  sssnm  3832  ssiun  4007  ssiun2  4008  disjnim  4073  exmidsssnc  4287  sotricim  4414  sotritrieq  4416  tron  4473  ordsucss  4596  ordunisuc2r  4606  ordpwsucss  4659  dmcosseq  4996  relssres  5043  trin2  5120  ssrnres  5171  fnun  5429  f1oun  5594  ssimaex  5697  chfnrn  5748  dffo4  5785  dffo5  5786  isoselem  5950  fnoprabg  6111  poxp  6384  issmo2  6441  smores  6444  tfr0dm  6474  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  swoer  6716  qsss  6749  findcard  7058  findcard2  7059  findcard2s  7060  supmoti  7168  ctmlemr  7283  ctm  7284  pm54.43  7371  indpi  7537  recexprlemm  7819  recexprlemloc  7826  recexprlem1ssl  7828  recexprlem1ssu  7829  recexprlemss1l  7830  recexprlemss1u  7831  zmulcl  9508  indstr  9796  eluzdc  9813  icoshft  10194  fzouzsplit  10385  seqf1oglem1  10749  seqf1oglem2  10750  hashunlem  11034  modfsummod  11977  dvds2lem  12322  oddnn02np1  12399  dfgcd2  12543  sqrt2irr  12692  ennnfonelemhom  12994  omctfn  13022  ptex  13305  kerf1ghm  13819  rmodislmodlem  14322  distop  14767  epttop  14772  restdis  14866  cnrest2  14918  cnptopresti  14920  uptx  14956  txcn  14957  logbgcd1irr  15649  gausslemma2dlem1a  15745  2sqlem10  15812  decidr  16184  bj-charfunbi  16198  bj-omssind  16322  bj-om  16324  bj-inf2vnlem3  16359  bj-inf2vnlem4  16360