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  942  oplem1  981  3impexpbicom  1481  hband  1535  hb3and  1536  nfand  1614  nfimd  1631  equsexd  1775  euim  2146  mopick2  2161  2moswapdc  2168  necon3bd  2443  necon3d  2444  necon2ad  2457  necon1abiddc  2462  ralrimd  2608  rspcimedv  2909  2reuswapdc  3007  ra5  3118  difin  3441  r19.2m  3578  r19.2mOLD  3579  tpid3g  3782  sssnm  3832  ssiun  4007  ssiun2  4008  disjnim  4073  exmidsssnc  4287  sotricim  4414  sotritrieq  4416  tron  4473  ordsucss  4596  ordunisuc2r  4606  ordpwsucss  4659  dmcosseq  4996  relssres  5043  trin2  5120  ssrnres  5171  fnun  5429  f1oun  5594  ssimaex  5697  chfnrn  5748  dffo4  5785  dffo5  5786  isoselem  5950  fnoprabg  6111  poxp  6384  issmo2  6441  smores  6444  tfr0dm  6474  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  swoer  6716  qsss  6749  findcard  7058  findcard2  7059  findcard2s  7060  supmoti  7171  ctmlemr  7286  ctm  7287  pm54.43  7374  indpi  7540  recexprlemm  7822  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1l  7833  recexprlemss1u  7834  zmulcl  9511  indstr  9800  eluzdc  9817  icoshft  10198  fzouzsplit  10389  seqf1oglem1  10753  seqf1oglem2  10754  hashunlem  11038  modfsummod  11984  dvds2lem  12329  oddnn02np1  12406  dfgcd2  12550  sqrt2irr  12699  ennnfonelemhom  13001  omctfn  13029  ptex  13312  kerf1ghm  13826  rmodislmodlem  14329  distop  14774  epttop  14779  restdis  14873  cnrest2  14925  cnptopresti  14927  uptx  14963  txcn  14964  logbgcd1irr  15656  gausslemma2dlem1a  15752  2sqlem10  15819  vtxdumgrfival  16057  decidr  16215  bj-charfunbi  16229  bj-omssind  16353  bj-om  16355  bj-inf2vnlem3  16390  bj-inf2vnlem4  16391