Theorem syl6ibr 160

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 131	. 2 |- ( ch -> th )
4	1, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr4g  203  imp4a  341  dcbi  877  oplem1  916  3impexpbicom  1367  hband  1418  hb3and  1419  nfand  1500  nfimd  1517  equsexd  1657  euim  2009  mopick2  2024  2moswapdc  2031  necon3bd  2288  necon3d  2289  necon2ad  2302  necon1abiddc  2307  ralrimd  2439  rspcimedv  2703  2reuswapdc  2794  ra5  2902  difin  3201  r19.2m  3329  tpid3g  3505  sssnm  3546  ssiun  3720  ssiun2  3721  sotricim  4078  sotritrieq  4080  tron  4137  ordsucss  4248  ordunisuc2r  4258  ordpwsucss  4310  dmcosseq  4621  relssres  4666  trin2  4736  ssrnres  4783  fnun  5025  f1oun  5166  ssimaex  5255  chfnrn  5299  dffo4  5336  dffo5  5337  isoselem  5479  fnoprabg  5622  poxp  5873  issmo2  5927  smores  5930  tfr0  5960  tfrlemibxssdm  5964  swoer  6157  qsss  6188  findcard  6372  findcard2  6373  findcard2s  6374  supmoti  6406  pm54.43  6459  indpi  6532  recexprlemm  6814  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  recexprlemss1l  6825  recexprlemss1u  6826  zmulcl  8404  indstr  8681  eluzdc  8697  icoshft  9012  fzouzsplit  9188  dvds2lem  10207  oddnn02np1  10280  dfgcd2  10403  sqrt2irr  10541  bj-omssind  10730  bj-om  10732  bj-inf2vnlem3  10767  bj-inf2vnlem4  10768