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  347  dcbi  926  oplem1  965  3impexpbicom  1426  hband  1477  hb3and  1478  nfand  1556  nfimd  1573  equsexd  1717  euim  2082  mopick2  2097  2moswapdc  2104  necon3bd  2379  necon3d  2380  necon2ad  2393  necon1abiddc  2398  ralrimd  2544  rspcimedv  2832  2reuswapdc  2930  ra5  3039  difin  3359  r19.2m  3495  r19.2mOLD  3496  tpid3g  3691  sssnm  3734  ssiun  3908  ssiun2  3909  disjnim  3973  exmidsssnc  4182  sotricim  4301  sotritrieq  4303  tron  4360  ordsucss  4481  ordunisuc2r  4491  ordpwsucss  4544  dmcosseq  4875  relssres  4922  trin2  4995  ssrnres  5046  fnun  5294  f1oun  5452  ssimaex  5547  chfnrn  5596  dffo4  5633  dffo5  5634  isoselem  5788  fnoprabg  5943  poxp  6200  issmo2  6257  smores  6260  tfr0dm  6290  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  swoer  6529  qsss  6560  findcard  6854  findcard2  6855  findcard2s  6856  supmoti  6958  ctmlemr  7073  ctm  7074  pm54.43  7146  indpi  7283  recexprlemm  7565  recexprlemloc  7572  recexprlem1ssl  7574  recexprlem1ssu  7575  recexprlemss1l  7576  recexprlemss1u  7577  zmulcl  9244  indstr  9531  eluzdc  9548  icoshft  9926  fzouzsplit  10114  hashunlem  10717  modfsummod  11399  dvds2lem  11743  oddnn02np1  11817  dfgcd2  11947  sqrt2irr  12094  ennnfonelemhom  12348  omctfn  12376  distop  12725  epttop  12730  restdis  12824  cnrest2  12876  cnptopresti  12878  uptx  12914  txcn  12915  logbgcd1irr  13525  2sqlem10  13601  decidr  13677  bj-charfunbi  13693  bj-omssind  13817  bj-om  13819  bj-inf2vnlem3  13854  bj-inf2vnlem4  13855