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	|- ( ph -> ( ps -> ch ) )
imbitrrdi.2	|- ( th <-> ch )

Assertion

Ref	Expression
imbitrrdi	|- ( ph -> ( ps -> th ) )

Proof of Theorem imbitrrdi

Step	Hyp	Ref	Expression
1		imbitrrdi.1	. 2 |- ( ph -> ( ps -> ch ) )
2		imbitrrdi.2	. . 3 |- ( th <-> ch )
3	2	biimpri 133	. 2 |- ( ch -> th )
4	1, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

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  2883  2reuswapdc  2981  ra5  3091  difin  3414  r19.2m  3551  r19.2mOLD  3552  tpid3g  3753  sssnm  3803  ssiun  3978  ssiun2  3979  disjnim  4044  exmidsssnc  4258  sotricim  4383  sotritrieq  4385  tron  4442  ordsucss  4565  ordunisuc2r  4575  ordpwsucss  4628  dmcosseq  4964  relssres  5011  trin2  5088  ssrnres  5139  fnun  5396  f1oun  5559  ssimaex  5658  chfnrn  5709  dffo4  5746  dffo5  5747  isoselem  5907  fnoprabg  6064  poxp  6336  issmo2  6393  smores  6396  tfr0dm  6426  tfrlemibxssdm  6431  tfr1onlembxssdm  6447  tfrcllembxssdm  6460  swoer  6666  qsss  6699  findcard  7006  findcard2  7007  findcard2s  7008  supmoti  7116  ctmlemr  7231  ctm  7232  pm54.43  7319  indpi  7485  recexprlemm  7767  recexprlemloc  7774  recexprlem1ssl  7776  recexprlem1ssu  7777  recexprlemss1l  7778  recexprlemss1u  7779  zmulcl  9456  indstr  9744  eluzdc  9761  icoshft  10142  fzouzsplit  10333  seqf1oglem1  10696  seqf1oglem2  10697  hashunlem  10981  modfsummod  11854  dvds2lem  12199  oddnn02np1  12276  dfgcd2  12420  sqrt2irr  12569  ennnfonelemhom  12871  omctfn  12899  ptex  13181  kerf1ghm  13695  rmodislmodlem  14197  distop  14642  epttop  14647  restdis  14741  cnrest2  14793  cnptopresti  14795  uptx  14831  txcn  14832  logbgcd1irr  15524  gausslemma2dlem1a  15620  2sqlem10  15687  decidr  15902  bj-charfunbi  15916  bj-omssind  16040  bj-om  16042  bj-inf2vnlem3  16077  bj-inf2vnlem4  16078