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-mp 5  ax-1 6  ax-2 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  346  dcbi  920  oplem1  959  3impexpbicom  1414  hband  1465  hb3and  1466  nfand  1547  nfimd  1564  equsexd  1707  euim  2067  mopick2  2082  2moswapdc  2089  necon3bd  2351  necon3d  2352  necon2ad  2365  necon1abiddc  2370  ralrimd  2510  rspcimedv  2791  2reuswapdc  2888  ra5  2997  difin  3313  r19.2m  3449  r19.2mOLD  3450  tpid3g  3638  sssnm  3681  ssiun  3855  ssiun2  3856  disjnim  3920  exmidsssnc  4126  sotricim  4245  sotritrieq  4247  tron  4304  ordsucss  4420  ordunisuc2r  4430  ordpwsucss  4482  dmcosseq  4810  relssres  4857  trin2  4930  ssrnres  4981  fnun  5229  f1oun  5387  ssimaex  5482  chfnrn  5531  dffo4  5568  dffo5  5569  isoselem  5721  fnoprabg  5872  poxp  6129  issmo2  6186  smores  6189  tfr0dm  6219  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  swoer  6457  qsss  6488  findcard  6782  findcard2  6783  findcard2s  6784  supmoti  6880  ctmlemr  6993  ctm  6994  pm54.43  7046  indpi  7150  recexprlemm  7432  recexprlemloc  7439  recexprlem1ssl  7441  recexprlem1ssu  7442  recexprlemss1l  7443  recexprlemss1u  7444  zmulcl  9107  indstr  9388  eluzdc  9404  icoshft  9773  fzouzsplit  9956  hashunlem  10550  modfsummod  11227  dvds2lem  11505  oddnn02np1  11577  dfgcd2  11702  sqrt2irr  11840  ennnfonelemhom  11928  distop  12254  epttop  12259  restdis  12353  cnrest2  12405  cnptopresti  12407  uptx  12443  txcn  12444  decidr  13003  bj-omssind  13133  bj-om  13135  bj-inf2vnlem3  13170  bj-inf2vnlem4  13171