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  7252  ctmlemr  7367  ctm  7368  pm54.43  7455  indpi  7622  recexprlemm  7904  recexprlemloc  7911  recexprlem1ssl  7913  recexprlem1ssu  7914  recexprlemss1l  7915  recexprlemss1u  7916  zmulcl  9594  indstr  9888  eluzdc  9905  icoshft  10286  fzouzsplit  10478  seqf1oglem1  10844  seqf1oglem2  10845  hashunlem  11130  modfsummod  12099  dvds2lem  12444  oddnn02np1  12521  dfgcd2  12665  sqrt2irr  12814  ennnfonelemhom  13116  omctfn  13144  ptex  13427  kerf1ghm  13941  rmodislmodlem  14446  distop  14896  epttop  14901  restdis  14995  cnrest2  15047  cnptopresti  15049  uptx  15085  txcn  15086  logbgcd1irr  15778  gausslemma2dlem1a  15877  2sqlem10  15944  uhgrissubgr  16202  vtxdumgrfival  16239  decidr  16514  bj-charfunbi  16527  bj-omssind  16651  bj-om  16653  bj-inf2vnlem3  16688  bj-inf2vnlem4  16689