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	⊢ (𝜑 → (𝜓 → 𝜒))
syl6ibr.2	⊢ (𝜃 ↔ 𝜒)

Assertion

Ref	Expression
syl6ibr	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6ibr

Step	Hyp	Ref	Expression
1		syl6ibr.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6ibr.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	biimpri 132	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  931  oplem1  970  3impexpbicom  1431  hband  1482  hb3and  1483  nfand  1561  nfimd  1578  equsexd  1722  euim  2087  mopick2  2102  2moswapdc  2109  necon3bd  2383  necon3d  2384  necon2ad  2397  necon1abiddc  2402  ralrimd  2548  rspcimedv  2836  2reuswapdc  2934  ra5  3043  difin  3364  r19.2m  3501  r19.2mOLD  3502  tpid3g  3698  sssnm  3741  ssiun  3915  ssiun2  3916  disjnim  3980  exmidsssnc  4189  sotricim  4308  sotritrieq  4310  tron  4367  ordsucss  4488  ordunisuc2r  4498  ordpwsucss  4551  dmcosseq  4882  relssres  4929  trin2  5002  ssrnres  5053  fnun  5304  f1oun  5462  ssimaex  5557  chfnrn  5607  dffo4  5644  dffo5  5645  isoselem  5799  fnoprabg  5954  poxp  6211  issmo2  6268  smores  6271  tfr0dm  6301  tfrlemibxssdm  6306  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  swoer  6541  qsss  6572  findcard  6866  findcard2  6867  findcard2s  6868  supmoti  6970  ctmlemr  7085  ctm  7086  pm54.43  7167  indpi  7304  recexprlemm  7586  recexprlemloc  7593  recexprlem1ssl  7595  recexprlem1ssu  7596  recexprlemss1l  7597  recexprlemss1u  7598  zmulcl  9265  indstr  9552  eluzdc  9569  icoshft  9947  fzouzsplit  10135  hashunlem  10739  modfsummod  11421  dvds2lem  11765  oddnn02np1  11839  dfgcd2  11969  sqrt2irr  12116  ennnfonelemhom  12370  omctfn  12398  distop  12879  epttop  12884  restdis  12978  cnrest2  13030  cnptopresti  13032  uptx  13068  txcn  13069  logbgcd1irr  13679  2sqlem10  13755  decidr  13831  bj-charfunbi  13846  bj-omssind  13970  bj-om  13972  bj-inf2vnlem3  14007  bj-inf2vnlem4  14008