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  2910  2reuswapdc  3008  ra5  3119  difin  3442  r19.2m  3579  r19.2mOLD  3580  tpid3g  3785  sssnm  3835  ssiun  4010  ssiun2  4011  disjnim  4076  exmidsssnc  4291  sotricim  4418  sotritrieq  4420  tron  4477  ordsucss  4600  ordunisuc2r  4610  ordpwsucss  4663  dmcosseq  5002  relssres  5049  trin2  5126  ssrnres  5177  fnun  5435  f1oun  5600  ssimaex  5703  chfnrn  5754  dffo4  5791  dffo5  5792  isoselem  5956  fnoprabg  6117  poxp  6392  issmo2  6450  smores  6453  tfr0dm  6483  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  swoer  6725  qsss  6758  findcard  7072  findcard2  7073  findcard2s  7074  supmoti  7186  ctmlemr  7301  ctm  7302  pm54.43  7389  indpi  7555  recexprlemm  7837  recexprlemloc  7844  recexprlem1ssl  7846  recexprlem1ssu  7847  recexprlemss1l  7848  recexprlemss1u  7849  zmulcl  9526  indstr  9820  eluzdc  9837  icoshft  10218  fzouzsplit  10409  seqf1oglem1  10774  seqf1oglem2  10775  hashunlem  11060  modfsummod  12012  dvds2lem  12357  oddnn02np1  12434  dfgcd2  12578  sqrt2irr  12727  ennnfonelemhom  13029  omctfn  13057  ptex  13340  kerf1ghm  13854  rmodislmodlem  14357  distop  14802  epttop  14807  restdis  14901  cnrest2  14953  cnptopresti  14955  uptx  14991  txcn  14992  logbgcd1irr  15684  gausslemma2dlem1a  15780  2sqlem10  15847  vtxdumgrfival  16109  decidr  16342  bj-charfunbi  16356  bj-omssind  16480  bj-om  16482  bj-inf2vnlem3  16517  bj-inf2vnlem4  16518