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  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  7070  findcard2  7071  findcard2s  7072  supmoti  7183  ctmlemr  7298  ctm  7299  pm54.43  7386  indpi  7552  recexprlemm  7834  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  recexprlemss1l  7845  recexprlemss1u  7846  zmulcl  9523  indstr  9817  eluzdc  9834  icoshft  10215  fzouzsplit  10406  seqf1oglem1  10771  seqf1oglem2  10772  hashunlem  11057  modfsummod  12009  dvds2lem  12354  oddnn02np1  12431  dfgcd2  12575  sqrt2irr  12724  ennnfonelemhom  13026  omctfn  13054  ptex  13337  kerf1ghm  13851  rmodislmodlem  14354  distop  14799  epttop  14804  restdis  14898  cnrest2  14950  cnptopresti  14952  uptx  14988  txcn  14989  logbgcd1irr  15681  gausslemma2dlem1a  15777  2sqlem10  15844  vtxdumgrfival  16104  decidr  16328  bj-charfunbi  16342  bj-omssind  16466  bj-om  16468  bj-inf2vnlem3  16503  bj-inf2vnlem4  16504