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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4g  205  imp4a  349  dcbi  949  oplem1  988  3impexpbicom  1488  hband  1542  hb3and  1543  nfand  1621  nfimd  1638  equsexd  1782  euim  2155  mopick2  2170  2moswapdc  2177  necon3bd  2463  necon3d  2464  necon2ad  2477  necon1abiddc  2482  ralrimd  2628  rspcimedv  2931  2reuswapdc  3030  ra5  3141  difin  3468  r19.2m  3614  r19.2mOLD  3615  tpid3g  3828  sssnm  3879  ssiun  4054  ssiun2  4055  disjnim  4120  exmidsssnc  4340  sotricim  4468  sotritrieq  4470  tron  4527  ordsucss  4651  ordunisuc2r  4661  ordpwsucss  4714  dmcosseq  5054  relssres  5101  trin2  5179  ssrnres  5230  fnun  5489  f1oun  5659  ssimaex  5764  chfnrn  5820  dffo4  5856  dffo5  5857  isoselem  6026  fnoprabg  6189  poxp  6468  issmo2  6560  smores  6563  tfr0dm  6593  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  swoer  6835  qsss  6868  findcard  7192  findcard2  7193  findcard2s  7194  supmoti  7333  ctmlemr  7448  ctm  7449  pm54.43  7536  indpi  7709  recexprlemm  7991  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  zmulcl  9698  indstr  9993  eluzdc  10010  icoshft  10392  fzouzsplit  10588  seqf1oglem1  10956  seqf1oglem2  10957  hashunlem  11244  modfsummod  12225  dvds2lem  12570  oddnn02np1  12647  dfgcd2  12791  sqrt2irr  12940  ennnfonelemhom  13306  omctfn  13334  ptex  13618  kerf1ghm  14077  rmodislmodlem  14687  distop  15186  epttop  15191  restdis  15285  cnrest2  15337  cnptopresti  15339  uptx  15375  txcn  15376  logbgcd1irr  16069  gausslemma2dlem1a  16177  2sqlem10  16244  uhgrissubgr  16502  vtxdumgrfival  16539  decidr  16824  bj-charfunbi  16837  bj-omssind  16961  bj-om  16963  bj-inf2vnlem3  16998  bj-inf2vnlem4  16999