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  1503  hb3and  1504  nfand  1582  nfimd  1599  equsexd  1743  euim  2113  mopick2  2128  2moswapdc  2135  necon3bd  2410  necon3d  2411  necon2ad  2424  necon1abiddc  2429  ralrimd  2575  rspcimedv  2870  2reuswapdc  2968  ra5  3078  difin  3400  r19.2m  3537  r19.2mOLD  3538  tpid3g  3737  sssnm  3784  ssiun  3958  ssiun2  3959  disjnim  4024  exmidsssnc  4236  sotricim  4358  sotritrieq  4360  tron  4417  ordsucss  4540  ordunisuc2r  4550  ordpwsucss  4603  dmcosseq  4937  relssres  4984  trin2  5061  ssrnres  5112  fnun  5364  f1oun  5524  ssimaex  5622  chfnrn  5673  dffo4  5710  dffo5  5711  isoselem  5867  fnoprabg  6023  poxp  6290  issmo2  6347  smores  6350  tfr0dm  6380  tfrlemibxssdm  6385  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  swoer  6620  qsss  6653  findcard  6949  findcard2  6950  findcard2s  6951  supmoti  7059  ctmlemr  7174  ctm  7175  pm54.43  7257  indpi  7409  recexprlemm  7691  recexprlemloc  7698  recexprlem1ssl  7700  recexprlem1ssu  7701  recexprlemss1l  7702  recexprlemss1u  7703  zmulcl  9379  indstr  9667  eluzdc  9684  icoshft  10065  fzouzsplit  10255  seqf1oglem1  10611  seqf1oglem2  10612  hashunlem  10896  modfsummod  11623  dvds2lem  11968  oddnn02np1  12045  dfgcd2  12181  sqrt2irr  12330  ennnfonelemhom  12632  omctfn  12660  ptex  12935  kerf1ghm  13404  rmodislmodlem  13906  distop  14321  epttop  14326  restdis  14420  cnrest2  14472  cnptopresti  14474  uptx  14510  txcn  14511  logbgcd1irr  15203  gausslemma2dlem1a  15299  2sqlem10  15366  decidr  15442  bj-charfunbi  15457  bj-omssind  15581  bj-om  15583  bj-inf2vnlem3  15618  bj-inf2vnlem4  15619