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  4340  sotricim  4468  sotritrieq  4470  tron  4527  ordsucss  4651  ordunisuc2r  4661  ordpwsucss  4714  dmcosseq  5054  relssres  5101  trin2  5179  ssrnres  5230  fnun  5489  f1oun  5659  ssimaex  5764  chfnrn  5820  dffo4  5856  dffo5  5857  isoselem  6026  fnoprabg  6189  poxp  6468  issmo2  6560  smores  6563  tfr0dm  6593  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  swoer  6835  qsss  6868  findcard  7192  findcard2  7193  findcard2s  7194  supmoti  7334  ctmlemr  7449  ctm  7450  pm54.43  7537  indpi  7710  recexprlemm  7992  recexprlemloc  7999  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  recexprlemss1u  8004  zmulcl  9703  indstr  10003  eluzdc  10020  icoshft  10403  fzouzsplit  10599  seqf1oglem1  10971  seqf1oglem2  10972  hashunlem  11260  fiidxsupcl  12012  modfsummod  12244  dvds2lem  12589  oddnn02np1  12666  dfgcd2  12810  sqrt2irr  12960  ennnfonelemhom  13358  omctfn  13386  ptex  13671  kerf1ghm  14130  rmodislmodlem  14771  distop  15277  epttop  15282  restdis  15376  cnrest2  15428  cnptopresti  15430  uptx  15466  txcn  15467  logbgcd1irr  16164  gausslemma2dlem1a  16343  2sqlem10  16410  uhgrissubgr  16668  vtxdumgrfival  16705  decidr  16990  bj-charfunbi  17003  bj-omssind  17127  bj-om  17129  bj-inf2vnlem3  17164  bj-inf2vnlem4  17165