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  937  oplem1  976  3impexpbicom  1448  hband  1499  hb3and  1500  nfand  1578  nfimd  1595  equsexd  1739  euim  2104  mopick2  2119  2moswapdc  2126  necon3bd  2400  necon3d  2401  necon2ad  2414  necon1abiddc  2419  ralrimd  2565  rspcimedv  2855  2reuswapdc  2953  ra5  3063  difin  3384  r19.2m  3521  r19.2mOLD  3522  tpid3g  3719  sssnm  3766  ssiun  3940  ssiun2  3941  disjnim  4006  exmidsssnc  4215  sotricim  4335  sotritrieq  4337  tron  4394  ordsucss  4515  ordunisuc2r  4525  ordpwsucss  4578  dmcosseq  4910  relssres  4957  trin2  5032  ssrnres  5083  fnun  5334  f1oun  5493  ssimaex  5590  chfnrn  5640  dffo4  5677  dffo5  5678  isoselem  5834  fnoprabg  5989  poxp  6247  issmo2  6304  smores  6307  tfr0dm  6337  tfrlemibxssdm  6342  tfr1onlembxssdm  6358  tfrcllembxssdm  6371  swoer  6577  qsss  6608  findcard  6902  findcard2  6903  findcard2s  6904  supmoti  7006  ctmlemr  7121  ctm  7122  pm54.43  7203  indpi  7355  recexprlemm  7637  recexprlemloc  7644  recexprlem1ssl  7646  recexprlem1ssu  7647  recexprlemss1l  7648  recexprlemss1u  7649  zmulcl  9320  indstr  9607  eluzdc  9624  icoshft  10004  fzouzsplit  10193  hashunlem  10798  modfsummod  11480  dvds2lem  11824  oddnn02np1  11899  dfgcd2  12029  sqrt2irr  12176  ennnfonelemhom  12430  omctfn  12458  ptex  12731  rmodislmodlem  13539  distop  13881  epttop  13886  restdis  13980  cnrest2  14032  cnptopresti  14034  uptx  14070  txcn  14071  logbgcd1irr  14681  2sqlem10  14768  decidr  14844  bj-charfunbi  14859  bj-omssind  14983  bj-om  14985  bj-inf2vnlem3  15020  bj-inf2vnlem4  15021