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  2909  2reuswapdc  3007  ra5  3118  difin  3441  r19.2m  3578  r19.2mOLD  3579  tpid3g  3781  sssnm  3831  ssiun  4006  ssiun2  4007  disjnim  4072  exmidsssnc  4286  sotricim  4413  sotritrieq  4415  tron  4472  ordsucss  4595  ordunisuc2r  4605  ordpwsucss  4658  dmcosseq  4995  relssres  5042  trin2  5119  ssrnres  5170  fnun  5428  f1oun  5591  ssimaex  5694  chfnrn  5745  dffo4  5782  dffo5  5783  isoselem  5943  fnoprabg  6104  poxp  6376  issmo2  6433  smores  6436  tfr0dm  6466  tfrlemibxssdm  6471  tfr1onlembxssdm  6487  tfrcllembxssdm  6500  swoer  6706  qsss  6739  findcard  7046  findcard2  7047  findcard2s  7048  supmoti  7156  ctmlemr  7271  ctm  7272  pm54.43  7359  indpi  7525  recexprlemm  7807  recexprlemloc  7814  recexprlem1ssl  7816  recexprlem1ssu  7817  recexprlemss1l  7818  recexprlemss1u  7819  zmulcl  9496  indstr  9784  eluzdc  9801  icoshft  10182  fzouzsplit  10373  seqf1oglem1  10736  seqf1oglem2  10737  hashunlem  11021  modfsummod  11964  dvds2lem  12309  oddnn02np1  12386  dfgcd2  12530  sqrt2irr  12679  ennnfonelemhom  12981  omctfn  13009  ptex  13292  kerf1ghm  13806  rmodislmodlem  14308  distop  14753  epttop  14758  restdis  14852  cnrest2  14904  cnptopresti  14906  uptx  14942  txcn  14943  logbgcd1irr  15635  gausslemma2dlem1a  15731  2sqlem10  15798  decidr  16118  bj-charfunbi  16132  bj-omssind  16256  bj-om  16258  bj-inf2vnlem3  16293  bj-inf2vnlem4  16294