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  1777  euim  2148  mopick2  2163  2moswapdc  2170  necon3bd  2446  necon3d  2447  necon2ad  2460  necon1abiddc  2465  ralrimd  2611  rspcimedv  2913  2reuswapdc  3011  ra5  3122  difin  3446  r19.2m  3583  r19.2mOLD  3584  tpid3g  3791  sssnm  3842  ssiun  4017  ssiun2  4018  disjnim  4083  exmidsssnc  4299  sotricim  4426  sotritrieq  4428  tron  4485  ordsucss  4608  ordunisuc2r  4618  ordpwsucss  4671  dmcosseq  5010  relssres  5057  trin2  5135  ssrnres  5186  fnun  5445  f1oun  5612  ssimaex  5716  chfnrn  5767  dffo4  5803  dffo5  5804  isoselem  5971  fnoprabg  6132  poxp  6406  issmo2  6498  smores  6501  tfr0dm  6531  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  swoer  6773  qsss  6806  findcard  7120  findcard2  7121  findcard2s  7122  supmoti  7235  ctmlemr  7350  ctm  7351  pm54.43  7438  indpi  7605  recexprlemm  7887  recexprlemloc  7894  recexprlem1ssl  7896  recexprlem1ssu  7897  recexprlemss1l  7898  recexprlemss1u  7899  zmulcl  9577  indstr  9871  eluzdc  9888  icoshft  10269  fzouzsplit  10461  seqf1oglem1  10827  seqf1oglem2  10828  hashunlem  11113  modfsummod  12082  dvds2lem  12427  oddnn02np1  12504  dfgcd2  12648  sqrt2irr  12797  ennnfonelemhom  13099  omctfn  13127  ptex  13410  kerf1ghm  13924  rmodislmodlem  14429  distop  14879  epttop  14884  restdis  14978  cnrest2  15030  cnptopresti  15032  uptx  15068  txcn  15069  logbgcd1irr  15761  gausslemma2dlem1a  15860  2sqlem10  15927  uhgrissubgr  16185  vtxdumgrfival  16222  decidr  16497  bj-charfunbi  16510  bj-omssind  16634  bj-om  16636  bj-inf2vnlem3  16671  bj-inf2vnlem4  16672