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  945  oplem1  984  3impexpbicom  1484  hband  1538  hb3and  1539  nfand  1617  nfimd  1634  equsexd  1778  euim  2151  mopick2  2166  2moswapdc  2173  necon3bd  2457  necon3d  2458  necon2ad  2471  necon1abiddc  2476  ralrimd  2622  rspcimedv  2925  2reuswapdc  3024  ra5  3135  difin  3462  r19.2m  3600  r19.2mOLD  3601  tpid3g  3812  sssnm  3863  ssiun  4038  ssiun2  4039  disjnim  4104  exmidsssnc  4321  sotricim  4449  sotritrieq  4451  tron  4508  ordsucss  4631  ordunisuc2r  4641  ordpwsucss  4694  dmcosseq  5034  relssres  5081  trin2  5159  ssrnres  5210  fnun  5469  f1oun  5639  ssimaex  5743  chfnrn  5794  dffo4  5830  dffo5  5831  isoselem  5999  fnoprabg  6162  poxp  6441  issmo2  6533  smores  6536  tfr0dm  6566  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  swoer  6808  qsss  6841  findcard  7158  findcard2  7159  findcard2s  7160  supmoti  7297  ctmlemr  7412  ctm  7413  pm54.43  7500  indpi  7673  recexprlemm  7955  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  recexprlemss1u  7967  zmulcl  9648  indstr  9943  eluzdc  9960  icoshft  10342  fzouzsplit  10537  seqf1oglem1  10905  seqf1oglem2  10906  hashunlem  11193  modfsummod  12169  dvds2lem  12514  oddnn02np1  12591  dfgcd2  12735  sqrt2irr  12884  ennnfonelemhom  13250  omctfn  13278  ptex  13561  kerf1ghm  14027  rmodislmodlem  14624  distop  15076  epttop  15081  restdis  15175  cnrest2  15227  cnptopresti  15229  uptx  15265  txcn  15266  logbgcd1irr  15958  gausslemma2dlem1a  16057  2sqlem10  16124  uhgrissubgr  16382  vtxdumgrfival  16419  decidr  16694  bj-charfunbi  16707  bj-omssind  16831  bj-om  16833  bj-inf2vnlem3  16868  bj-inf2vnlem4  16869