Theorem syl6ibr 151

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3imtr4g  194  imp4a  331  dcbi  844  oplem1  882  3impexpbicom  1327  hband  1378  hb3and  1379  nfand  1460  nfimd  1477  equsexd  1617  euim  1968  mopick2  1983  2moswapdc  1990  necon3bd  2248  necon3d  2249  necon2ad  2262  necon1abiddc  2267  ralrimd  2397  rspcimedv  2658  2reuswapdc  2743  eqsbc3r  2819  ra5  2846  difin  3174  r19.2m  3309  tpid3g  3483  sssnm  3525  ssiun  3699  ssiun2  3700  sotricim  4060  sotritrieq  4062  tron  4119  ordsucss  4230  ordunisuc2r  4240  ordpwsucss  4291  dmcosseq  4603  relssres  4648  trin2  4716  ssrnres  4763  fnun  5005  f1oun  5146  ssimaex  5234  chfnrn  5278  dffo4  5315  dffo5  5316  isoselem  5459  fnoprabg  5602  poxp  5853  issmo2  5904  smores  5907  tfr0  5937  tfrlemibxssdm  5941  swoer  6134  qsss  6165  findcard  6345  findcard2  6346  findcard2s  6347  indpi  6440  recexprlemm  6722  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734  zmulcl  8297  indstr  8536  eluzdc  8547  icoshft  8858  fzouzsplit  9035  sqrt2irr  9878  bj-omssind  10059  bj-om  10061  bj-inf2vnlem3  10097  bj-inf2vnlem4  10098