Theorem syl6ibr 161

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
syl6ibr.1	|- ( ph -> ( ps -> ch ) )
syl6ibr.2	|- ( th <-> ch )

Assertion

Ref	Expression
syl6ibr	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6ibr

Step	Hyp	Ref	Expression
1		syl6ibr.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syl6ibr.2	. . 3 |- ( th <-> ch )
3	2	biimpri 132	. 2 |- ( ch -> th )
4	1, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4g  204  imp4a  344  dcbi  903  oplem1  942  3impexpbicom  1397  hband  1448  hb3and  1449  nfand  1530  nfimd  1547  equsexd  1690  euim  2043  mopick2  2058  2moswapdc  2065  necon3bd  2325  necon3d  2326  necon2ad  2339  necon1abiddc  2344  ralrimd  2484  rspcimedv  2762  2reuswapdc  2857  ra5  2965  difin  3279  r19.2m  3415  r19.2mOLD  3416  tpid3g  3604  sssnm  3647  ssiun  3821  ssiun2  3822  disjnim  3886  exmidsssnc  4086  sotricim  4205  sotritrieq  4207  tron  4264  ordsucss  4380  ordunisuc2r  4390  ordpwsucss  4442  dmcosseq  4768  relssres  4815  trin2  4888  ssrnres  4939  fnun  5187  f1oun  5343  ssimaex  5436  chfnrn  5485  dffo4  5522  dffo5  5523  isoselem  5675  fnoprabg  5826  poxp  6083  issmo2  6140  smores  6143  tfr0dm  6173  tfrlemibxssdm  6178  tfr1onlembxssdm  6194  tfrcllembxssdm  6207  swoer  6411  qsss  6442  findcard  6735  findcard2  6736  findcard2s  6737  supmoti  6832  ctmlemr  6945  ctm  6946  pm54.43  6996  indpi  7098  recexprlemm  7380  recexprlemloc  7387  recexprlem1ssl  7389  recexprlem1ssu  7390  recexprlemss1l  7391  recexprlemss1u  7392  zmulcl  9011  indstr  9290  eluzdc  9306  icoshft  9666  fzouzsplit  9849  hashunlem  10443  modfsummod  11119  dvds2lem  11353  oddnn02np1  11425  dfgcd2  11548  sqrt2irr  11686  ennnfonelemhom  11773  distop  12097  epttop  12102  restdis  12196  cnrest2  12247  cnptopresti  12249  uptx  12285  txcn  12286  decidr  12695  bj-omssind  12825  bj-om  12827  bj-inf2vnlem3  12862  bj-inf2vnlem4  12863