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  5960  fnoprabg  6121  poxp  6396  issmo2  6454  smores  6457  tfr0dm  6487  tfrlemibxssdm  6492  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  swoer  6729  qsss  6762  findcard  7076  findcard2  7077  findcard2s  7078  supmoti  7191  ctmlemr  7306  ctm  7307  pm54.43  7394  indpi  7561  recexprlemm  7843  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1l  7854  recexprlemss1u  7855  zmulcl  9532  indstr  9826  eluzdc  9843  icoshft  10224  fzouzsplit  10415  seqf1oglem1  10780  seqf1oglem2  10781  hashunlem  11066  modfsummod  12018  dvds2lem  12363  oddnn02np1  12440  dfgcd2  12584  sqrt2irr  12733  ennnfonelemhom  13035  omctfn  13063  ptex  13346  kerf1ghm  13860  rmodislmodlem  14363  distop  14808  epttop  14813  restdis  14907  cnrest2  14959  cnptopresti  14961  uptx  14997  txcn  14998  logbgcd1irr  15690  gausslemma2dlem1a  15786  2sqlem10  15853  uhgrissubgr  16111  vtxdumgrfival  16148  decidr  16392  bj-charfunbi  16406  bj-omssind  16530  bj-om  16532  bj-inf2vnlem3  16567  bj-inf2vnlem4  16568