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  944  oplem1  983  3impexpbicom  1483  hband  1537  hb3and  1538  nfand  1616  nfimd  1633  equsexd  1777  euim  2148  mopick2  2163  2moswapdc  2170  necon3bd  2445  necon3d  2446  necon2ad  2459  necon1abiddc  2464  ralrimd  2610  rspcimedv  2912  2reuswapdc  3010  ra5  3121  difin  3444  r19.2m  3581  r19.2mOLD  3582  tpid3g  3787  sssnm  3837  ssiun  4012  ssiun2  4013  disjnim  4078  exmidsssnc  4293  sotricim  4420  sotritrieq  4422  tron  4479  ordsucss  4602  ordunisuc2r  4612  ordpwsucss  4665  dmcosseq  5004  relssres  5051  trin2  5128  ssrnres  5179  fnun  5438  f1oun  5603  ssimaex  5707  chfnrn  5758  dffo4  5795  dffo5  5796  isoselem  5961  fnoprabg  6122  poxp  6397  issmo2  6455  smores  6458  tfr0dm  6488  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  swoer  6730  qsss  6763  findcard  7077  findcard2  7078  findcard2s  7079  supmoti  7192  ctmlemr  7307  ctm  7308  pm54.43  7395  indpi  7562  recexprlemm  7844  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  zmulcl  9533  indstr  9827  eluzdc  9844  icoshft  10225  fzouzsplit  10416  seqf1oglem1  10782  seqf1oglem2  10783  hashunlem  11068  modfsummod  12037  dvds2lem  12382  oddnn02np1  12459  dfgcd2  12603  sqrt2irr  12752  ennnfonelemhom  13054  omctfn  13082  ptex  13365  kerf1ghm  13879  rmodislmodlem  14383  distop  14828  epttop  14833  restdis  14927  cnrest2  14979  cnptopresti  14981  uptx  15017  txcn  15018  logbgcd1irr  15710  gausslemma2dlem1a  15806  2sqlem10  15873  uhgrissubgr  16131  vtxdumgrfival  16168  decidr  16443  bj-charfunbi  16457  bj-omssind  16581  bj-om  16583  bj-inf2vnlem3  16618  bj-inf2vnlem4  16619