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  6565  smores  6568  tfr0dm  6598  tfrlemibxssdm  6603  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  swoer  6840  qsss  6873  findcard  7198  findcard2  7199  findcard2s  7200  supmoti  7339  ctmlemr  7454  ctm  7455  pm54.43  7542  indpi  7715  recexprlemm  7997  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  zmulcl  9707  indstr  10008  eluzdc  10025  icoshft  10408  fzouzsplit  10604  seqf1oglem1  10976  seqf1oglem2  10977  hashunlem  11265  fiidxsupcl  12017  modfsummod  12249  dvds2lem  12594  oddnn02np1  12671  dfgcd2  12815  sqrt2irr  12965  ennnfonelemhom  13363  omctfn  13391  ptex  13676  kerf1ghm  14135  rmodislmodlem  14795  distop  15328  epttop  15333  restdis  15427  cnrest2  15479  cnptopresti  15481  uptx  15517  txcn  15518  logbgcd1irr  16220  gausslemma2dlem1a  16399  2sqlem10  16466  uhgrissubgr  16724  vtxdumgrfival  16761  decidr  17046  bj-charfunbi  17059  bj-omssind  17183  bj-om  17185  bj-inf2vnlem3  17220  bj-inf2vnlem4  17221