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  938  oplem1  977  3impexpbicom  1449  hband  1500  hb3and  1501  nfand  1579  nfimd  1596  equsexd  1740  euim  2110  mopick2  2125  2moswapdc  2132  necon3bd  2407  necon3d  2408  necon2ad  2421  necon1abiddc  2426  ralrimd  2572  rspcimedv  2866  2reuswapdc  2964  ra5  3074  difin  3396  r19.2m  3533  r19.2mOLD  3534  tpid3g  3733  sssnm  3780  ssiun  3954  ssiun2  3955  disjnim  4020  exmidsssnc  4232  sotricim  4354  sotritrieq  4356  tron  4413  ordsucss  4536  ordunisuc2r  4546  ordpwsucss  4599  dmcosseq  4933  relssres  4980  trin2  5057  ssrnres  5108  fnun  5360  f1oun  5520  ssimaex  5618  chfnrn  5669  dffo4  5706  dffo5  5707  isoselem  5863  fnoprabg  6019  poxp  6285  issmo2  6342  smores  6345  tfr0dm  6375  tfrlemibxssdm  6380  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  swoer  6615  qsss  6648  findcard  6944  findcard2  6945  findcard2s  6946  supmoti  7052  ctmlemr  7167  ctm  7168  pm54.43  7250  indpi  7402  recexprlemm  7684  recexprlemloc  7691  recexprlem1ssl  7693  recexprlem1ssu  7694  recexprlemss1l  7695  recexprlemss1u  7696  zmulcl  9370  indstr  9658  eluzdc  9675  icoshft  10056  fzouzsplit  10246  seqf1oglem1  10590  seqf1oglem2  10591  hashunlem  10875  modfsummod  11601  dvds2lem  11946  oddnn02np1  12021  dfgcd2  12151  sqrt2irr  12300  ennnfonelemhom  12572  omctfn  12600  ptex  12875  kerf1ghm  13344  rmodislmodlem  13846  distop  14253  epttop  14258  restdis  14352  cnrest2  14404  cnptopresti  14406  uptx  14442  txcn  14443  logbgcd1irr  15099  gausslemma2dlem1a  15174  2sqlem10  15212  decidr  15288  bj-charfunbi  15303  bj-omssind  15427  bj-om  15429  bj-inf2vnlem3  15464  bj-inf2vnlem4  15465