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  1457  hband  1511  hb3and  1512  nfand  1590  nfimd  1607  equsexd  1751  euim  2121  mopick2  2136  2moswapdc  2143  necon3bd  2418  necon3d  2419  necon2ad  2432  necon1abiddc  2437  ralrimd  2583  rspcimedv  2878  2reuswapdc  2976  ra5  3086  difin  3409  r19.2m  3546  r19.2mOLD  3547  tpid3g  3747  sssnm  3794  ssiun  3968  ssiun2  3969  disjnim  4034  exmidsssnc  4246  sotricim  4369  sotritrieq  4371  tron  4428  ordsucss  4551  ordunisuc2r  4561  ordpwsucss  4614  dmcosseq  4949  relssres  4996  trin2  5073  ssrnres  5124  fnun  5381  f1oun  5541  ssimaex  5639  chfnrn  5690  dffo4  5727  dffo5  5728  isoselem  5888  fnoprabg  6045  poxp  6317  issmo2  6374  smores  6377  tfr0dm  6407  tfrlemibxssdm  6412  tfr1onlembxssdm  6428  tfrcllembxssdm  6441  swoer  6647  qsss  6680  findcard  6984  findcard2  6985  findcard2s  6986  supmoti  7094  ctmlemr  7209  ctm  7210  pm54.43  7297  indpi  7454  recexprlemm  7736  recexprlemloc  7743  recexprlem1ssl  7745  recexprlem1ssu  7746  recexprlemss1l  7747  recexprlemss1u  7748  zmulcl  9425  indstr  9713  eluzdc  9730  icoshft  10111  fzouzsplit  10301  seqf1oglem1  10662  seqf1oglem2  10663  hashunlem  10947  modfsummod  11740  dvds2lem  12085  oddnn02np1  12162  dfgcd2  12306  sqrt2irr  12455  ennnfonelemhom  12757  omctfn  12785  ptex  13067  kerf1ghm  13581  rmodislmodlem  14083  distop  14528  epttop  14533  restdis  14627  cnrest2  14679  cnptopresti  14681  uptx  14717  txcn  14718  logbgcd1irr  15410  gausslemma2dlem1a  15506  2sqlem10  15573  decidr  15694  bj-charfunbi  15709  bj-omssind  15833  bj-om  15835  bj-inf2vnlem3  15870  bj-inf2vnlem4  15871