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  936  oplem1  975  3impexpbicom  1438  hband  1489  hb3and  1490  nfand  1568  nfimd  1585  equsexd  1729  euim  2094  mopick2  2109  2moswapdc  2116  necon3bd  2390  necon3d  2391  necon2ad  2404  necon1abiddc  2409  ralrimd  2555  rspcimedv  2845  2reuswapdc  2943  ra5  3053  difin  3374  r19.2m  3511  r19.2mOLD  3512  tpid3g  3709  sssnm  3756  ssiun  3930  ssiun2  3931  disjnim  3996  exmidsssnc  4205  sotricim  4325  sotritrieq  4327  tron  4384  ordsucss  4505  ordunisuc2r  4515  ordpwsucss  4568  dmcosseq  4900  relssres  4947  trin2  5022  ssrnres  5073  fnun  5324  f1oun  5483  ssimaex  5579  chfnrn  5629  dffo4  5666  dffo5  5667  isoselem  5823  fnoprabg  5978  poxp  6235  issmo2  6292  smores  6295  tfr0dm  6325  tfrlemibxssdm  6330  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  swoer  6565  qsss  6596  findcard  6890  findcard2  6891  findcard2s  6892  supmoti  6994  ctmlemr  7109  ctm  7110  pm54.43  7191  indpi  7343  recexprlemm  7625  recexprlemloc  7632  recexprlem1ssl  7634  recexprlem1ssu  7635  recexprlemss1l  7636  recexprlemss1u  7637  zmulcl  9308  indstr  9595  eluzdc  9612  icoshft  9992  fzouzsplit  10181  hashunlem  10786  modfsummod  11468  dvds2lem  11812  oddnn02np1  11887  dfgcd2  12017  sqrt2irr  12164  ennnfonelemhom  12418  omctfn  12446  ptex  12718  rmodislmodlem  13445  distop  13624  epttop  13629  restdis  13723  cnrest2  13775  cnptopresti  13777  uptx  13813  txcn  13814  logbgcd1irr  14424  2sqlem10  14511  decidr  14587  bj-charfunbi  14602  bj-omssind  14726  bj-om  14728  bj-inf2vnlem3  14763  bj-inf2vnlem4  14764