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  4288  sotricim  4415  sotritrieq  4417  tron  4474  ordsucss  4597  ordunisuc2r  4607  ordpwsucss  4660  dmcosseq  4999  relssres  5046  trin2  5123  ssrnres  5174  fnun  5432  f1oun  5597  ssimaex  5700  chfnrn  5751  dffo4  5788  dffo5  5789  isoselem  5953  fnoprabg  6114  poxp  6389  issmo2  6446  smores  6449  tfr0dm  6479  tfrlemibxssdm  6484  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  swoer  6721  qsss  6754  findcard  7063  findcard2  7064  findcard2s  7065  supmoti  7176  ctmlemr  7291  ctm  7292  pm54.43  7379  indpi  7545  recexprlemm  7827  recexprlemloc  7834  recexprlem1ssl  7836  recexprlem1ssu  7837  recexprlemss1l  7838  recexprlemss1u  7839  zmulcl  9516  indstr  9805  eluzdc  9822  icoshft  10203  fzouzsplit  10394  seqf1oglem1  10758  seqf1oglem2  10759  hashunlem  11043  modfsummod  11990  dvds2lem  12335  oddnn02np1  12412  dfgcd2  12556  sqrt2irr  12705  ennnfonelemhom  13007  omctfn  13035  ptex  13318  kerf1ghm  13832  rmodislmodlem  14335  distop  14780  epttop  14785  restdis  14879  cnrest2  14931  cnptopresti  14933  uptx  14969  txcn  14970  logbgcd1irr  15662  gausslemma2dlem1a  15758  2sqlem10  15825  vtxdumgrfival  16084  decidr  16269  bj-charfunbi  16283  bj-omssind  16407  bj-om  16409  bj-inf2vnlem3  16444  bj-inf2vnlem4  16445