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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4g  205  imp4a  349  dcbi  949  oplem1  988  3impexpbicom  1488  hband  1542  hb3and  1543  nfand  1621  nfimd  1638  equsexd  1782  euim  2155  mopick2  2170  2moswapdc  2177  necon3bd  2463  necon3d  2464  necon2ad  2477  necon1abiddc  2482  ralrimd  2628  rspcimedv  2931  2reuswapdc  3030  ra5  3141  difin  3468  r19.2m  3614  r19.2mOLD  3615  tpid3g  3828  sssnm  3879  ssiun  4054  ssiun2  4055  disjnim  4120  exmidsssnc  4342  sotricim  4470  sotritrieq  4472  tron  4529  ordsucss  4653  ordunisuc2r  4663  ordpwsucss  4716  dmcosseq  5056  relssres  5103  trin2  5182  ssrnres  5233  fnun  5492  f1oun  5662  ssimaex  5767  chfnrn  5823  dffo4  5859  dffo5  5860  isoselem  6029  fnoprabg  6192  poxp  6472  issmo2  6564  smores  6567  tfr0dm  6597  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  swoer  6839  qsss  6872  findcard  7196  findcard2  7197  findcard2s  7198  supmoti  7339  ctmlemr  7454  ctm  7455  pm54.43  7542  indpi  7715  recexprlemm  7997  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  zmulcl  9709  indstr  10009  eluzdc  10026  icoshft  10409  fzouzsplit  10605  seqf1oglem1  10977  seqf1oglem2  10978  hashunlem  11266  fiidxsupcl  12018  modfsummod  12250  dvds2lem  12595  oddnn02np1  12672  dfgcd2  12816  sqrt2irr  12966  ennnfonelemhom  13364  omctfn  13392  ptex  13677  kerf1ghm  14136  rmodislmodlem  14796  distop  15311  epttop  15316  restdis  15410  cnrest2  15462  cnptopresti  15464  uptx  15500  txcn  15501  logbgcd1irr  16203  gausslemma2dlem1a  16382  2sqlem10  16449  uhgrissubgr  16707  vtxdumgrfival  16744  decidr  17029  bj-charfunbi  17042  bj-omssind  17166  bj-om  17168  bj-inf2vnlem3  17203  bj-inf2vnlem4  17204