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  2149  mopick2  2164  2moswapdc  2171  necon3bd  2455  necon3d  2456  necon2ad  2469  necon1abiddc  2474  ralrimd  2620  rspcimedv  2923  2reuswapdc  3021  ra5  3132  difin  3458  r19.2m  3596  r19.2mOLD  3597  tpid3g  3807  sssnm  3858  ssiun  4033  ssiun2  4034  disjnim  4099  exmidsssnc  4316  sotricim  4444  sotritrieq  4446  tron  4503  ordsucss  4626  ordunisuc2r  4636  ordpwsucss  4689  dmcosseq  5029  relssres  5076  trin2  5154  ssrnres  5205  fnun  5464  f1oun  5634  ssimaex  5738  chfnrn  5789  dffo4  5825  dffo5  5826  isoselem  5993  fnoprabg  6154  poxp  6428  issmo2  6520  smores  6523  tfr0dm  6553  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  swoer  6795  qsss  6828  findcard  7145  findcard2  7146  findcard2s  7147  supmoti  7284  ctmlemr  7399  ctm  7400  pm54.43  7487  indpi  7657  recexprlemm  7939  recexprlemloc  7946  recexprlem1ssl  7948  recexprlem1ssu  7949  recexprlemss1l  7950  recexprlemss1u  7951  zmulcl  9631  indstr  9925  eluzdc  9942  icoshft  10323  fzouzsplit  10515  seqf1oglem1  10881  seqf1oglem2  10882  hashunlem  11168  modfsummod  12144  dvds2lem  12489  oddnn02np1  12566  dfgcd2  12710  sqrt2irr  12859  ennnfonelemhom  13166  omctfn  13194  ptex  13477  kerf1ghm  13991  rmodislmodlem  14498  distop  14950  epttop  14955  restdis  15049  cnrest2  15101  cnptopresti  15103  uptx  15139  txcn  15140  logbgcd1irr  15832  gausslemma2dlem1a  15931  2sqlem10  15998  uhgrissubgr  16256  vtxdumgrfival  16293  decidr  16568  bj-charfunbi  16581  bj-omssind  16705  bj-om  16707  bj-inf2vnlem3  16742  bj-inf2vnlem4  16743