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  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  3611  r19.2mOLD  3612  tpid3g  3823  sssnm  3874  ssiun  4049  ssiun2  4050  disjnim  4115  exmidsssnc  4335  sotricim  4463  sotritrieq  4465  tron  4522  ordsucss  4646  ordunisuc2r  4656  ordpwsucss  4709  dmcosseq  5049  relssres  5096  trin2  5174  ssrnres  5225  fnun  5484  f1oun  5654  ssimaex  5758  chfnrn  5811  dffo4  5847  dffo5  5848  isoselem  6016  fnoprabg  6179  poxp  6458  issmo2  6550  smores  6553  tfr0dm  6583  tfrlemibxssdm  6588  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  swoer  6825  qsss  6858  findcard  7182  findcard2  7183  findcard2s  7184  supmoti  7323  ctmlemr  7438  ctm  7439  pm54.43  7526  indpi  7699  recexprlemm  7981  recexprlemloc  7988  recexprlem1ssl  7990  recexprlem1ssu  7991  recexprlemss1l  7992  recexprlemss1u  7993  zmulcl  9677  indstr  9972  eluzdc  9989  icoshft  10371  fzouzsplit  10566  seqf1oglem1  10934  seqf1oglem2  10935  hashunlem  11222  modfsummod  12203  dvds2lem  12548  oddnn02np1  12625  dfgcd2  12769  sqrt2irr  12918  ennnfonelemhom  13284  omctfn  13312  ptex  13595  kerf1ghm  14054  rmodislmodlem  14659  distop  15109  epttop  15114  restdis  15208  cnrest2  15260  cnptopresti  15262  uptx  15298  txcn  15299  logbgcd1irr  15992  gausslemma2dlem1a  16091  2sqlem10  16158  uhgrissubgr  16416  vtxdumgrfival  16453  decidr  16738  bj-charfunbi  16751  bj-omssind  16875  bj-om  16877  bj-inf2vnlem3  16912  bj-inf2vnlem4  16913