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  938  oplem1  977  3impexpbicom  1449  hband  1503  hb3and  1504  nfand  1582  nfimd  1599  equsexd  1743  euim  2113  mopick2  2128  2moswapdc  2135  necon3bd  2410  necon3d  2411  necon2ad  2424  necon1abiddc  2429  ralrimd  2575  rspcimedv  2870  2reuswapdc  2968  ra5  3078  difin  3401  r19.2m  3538  r19.2mOLD  3539  tpid3g  3738  sssnm  3785  ssiun  3959  ssiun2  3960  disjnim  4025  exmidsssnc  4237  sotricim  4359  sotritrieq  4361  tron  4418  ordsucss  4541  ordunisuc2r  4551  ordpwsucss  4604  dmcosseq  4938  relssres  4985  trin2  5062  ssrnres  5113  fnun  5367  f1oun  5527  ssimaex  5625  chfnrn  5676  dffo4  5713  dffo5  5714  isoselem  5870  fnoprabg  6027  poxp  6299  issmo2  6356  smores  6359  tfr0dm  6389  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  swoer  6629  qsss  6662  findcard  6958  findcard2  6959  findcard2s  6960  supmoti  7068  ctmlemr  7183  ctm  7184  pm54.43  7269  indpi  7426  recexprlemm  7708  recexprlemloc  7715  recexprlem1ssl  7717  recexprlem1ssu  7718  recexprlemss1l  7719  recexprlemss1u  7720  zmulcl  9396  indstr  9684  eluzdc  9701  icoshft  10082  fzouzsplit  10272  seqf1oglem1  10628  seqf1oglem2  10629  hashunlem  10913  modfsummod  11640  dvds2lem  11985  oddnn02np1  12062  dfgcd2  12206  sqrt2irr  12355  ennnfonelemhom  12657  omctfn  12685  ptex  12966  kerf1ghm  13480  rmodislmodlem  13982  distop  14405  epttop  14410  restdis  14504  cnrest2  14556  cnptopresti  14558  uptx  14594  txcn  14595  logbgcd1irr  15287  gausslemma2dlem1a  15383  2sqlem10  15450  decidr  15526  bj-charfunbi  15541  bj-omssind  15665  bj-om  15667  bj-inf2vnlem3  15702  bj-inf2vnlem4  15703