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  1458  hband  1512  hb3and  1513  nfand  1591  nfimd  1608  equsexd  1752  euim  2122  mopick2  2137  2moswapdc  2144  necon3bd  2419  necon3d  2420  necon2ad  2433  necon1abiddc  2438  ralrimd  2584  rspcimedv  2879  2reuswapdc  2977  ra5  3087  difin  3410  r19.2m  3547  r19.2mOLD  3548  tpid3g  3748  sssnm  3795  ssiun  3969  ssiun2  3970  disjnim  4035  exmidsssnc  4247  sotricim  4370  sotritrieq  4372  tron  4429  ordsucss  4552  ordunisuc2r  4562  ordpwsucss  4615  dmcosseq  4950  relssres  4997  trin2  5074  ssrnres  5125  fnun  5382  f1oun  5542  ssimaex  5640  chfnrn  5691  dffo4  5728  dffo5  5729  isoselem  5889  fnoprabg  6046  poxp  6318  issmo2  6375  smores  6378  tfr0dm  6408  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  swoer  6648  qsss  6681  findcard  6985  findcard2  6986  findcard2s  6987  supmoti  7095  ctmlemr  7210  ctm  7211  pm54.43  7298  indpi  7455  recexprlemm  7737  recexprlemloc  7744  recexprlem1ssl  7746  recexprlem1ssu  7747  recexprlemss1l  7748  recexprlemss1u  7749  zmulcl  9426  indstr  9714  eluzdc  9731  icoshft  10112  fzouzsplit  10303  seqf1oglem1  10664  seqf1oglem2  10665  hashunlem  10949  modfsummod  11769  dvds2lem  12114  oddnn02np1  12191  dfgcd2  12335  sqrt2irr  12484  ennnfonelemhom  12786  omctfn  12814  ptex  13096  kerf1ghm  13610  rmodislmodlem  14112  distop  14557  epttop  14562  restdis  14656  cnrest2  14708  cnptopresti  14710  uptx  14746  txcn  14747  logbgcd1irr  15439  gausslemma2dlem1a  15535  2sqlem10  15602  decidr  15732  bj-charfunbi  15747  bj-omssind  15871  bj-om  15873  bj-inf2vnlem3  15908  bj-inf2vnlem4  15909