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  921  oplem1  960  3impexpbicom  1415  hband  1466  hb3and  1467  nfand  1548  nfimd  1565  equsexd  1708  euim  2068  mopick2  2083  2moswapdc  2090  necon3bd  2352  necon3d  2353  necon2ad  2366  necon1abiddc  2371  ralrimd  2513  rspcimedv  2795  2reuswapdc  2892  ra5  3001  difin  3318  r19.2m  3454  r19.2mOLD  3455  tpid3g  3646  sssnm  3689  ssiun  3863  ssiun2  3864  disjnim  3928  exmidsssnc  4134  sotricim  4253  sotritrieq  4255  tron  4312  ordsucss  4428  ordunisuc2r  4438  ordpwsucss  4490  dmcosseq  4818  relssres  4865  trin2  4938  ssrnres  4989  fnun  5237  f1oun  5395  ssimaex  5490  chfnrn  5539  dffo4  5576  dffo5  5577  isoselem  5729  fnoprabg  5880  poxp  6137  issmo2  6194  smores  6197  tfr0dm  6227  tfrlemibxssdm  6232  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  swoer  6465  qsss  6496  findcard  6790  findcard2  6791  findcard2s  6792  supmoti  6888  ctmlemr  7001  ctm  7002  pm54.43  7063  indpi  7174  recexprlemm  7456  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  recexprlemss1l  7467  recexprlemss1u  7468  zmulcl  9131  indstr  9415  eluzdc  9431  icoshft  9803  fzouzsplit  9987  hashunlem  10582  modfsummod  11259  dvds2lem  11541  oddnn02np1  11613  dfgcd2  11738  sqrt2irr  11876  ennnfonelemhom  11964  omctfn  11992  distop  12293  epttop  12298  restdis  12392  cnrest2  12444  cnptopresti  12446  uptx  12482  txcn  12483  logbgcd1irr  13092  decidr  13174  bj-omssind  13304  bj-om  13306  bj-inf2vnlem3  13341  bj-inf2vnlem4  13342