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  1418  hband  1469  hb3and  1470  nfand  1548  nfimd  1565  equsexd  1709  euim  2074  mopick2  2089  2moswapdc  2096  necon3bd  2370  necon3d  2371  necon2ad  2384  necon1abiddc  2389  ralrimd  2535  rspcimedv  2818  2reuswapdc  2916  ra5  3025  difin  3344  r19.2m  3480  r19.2mOLD  3481  tpid3g  3675  sssnm  3718  ssiun  3892  ssiun2  3893  disjnim  3957  exmidsssnc  4165  sotricim  4284  sotritrieq  4286  tron  4343  ordsucss  4464  ordunisuc2r  4474  ordpwsucss  4527  dmcosseq  4858  relssres  4905  trin2  4978  ssrnres  5029  fnun  5277  f1oun  5435  ssimaex  5530  chfnrn  5579  dffo4  5616  dffo5  5617  isoselem  5771  fnoprabg  5923  poxp  6180  issmo2  6237  smores  6240  tfr0dm  6270  tfrlemibxssdm  6275  tfr1onlembxssdm  6291  tfrcllembxssdm  6304  swoer  6509  qsss  6540  findcard  6834  findcard2  6835  findcard2s  6836  supmoti  6938  ctmlemr  7053  ctm  7054  pm54.43  7126  indpi  7263  recexprlemm  7545  recexprlemloc  7552  recexprlem1ssl  7554  recexprlem1ssu  7555  recexprlemss1l  7556  recexprlemss1u  7557  zmulcl  9221  indstr  9505  eluzdc  9522  icoshft  9895  fzouzsplit  10082  hashunlem  10682  modfsummod  11359  dvds2lem  11703  oddnn02np1  11775  dfgcd2  11902  sqrt2irr  12041  ennnfonelemhom  12186  omctfn  12214  distop  12527  epttop  12532  restdis  12626  cnrest2  12678  cnptopresti  12680  uptx  12716  txcn  12717  logbgcd1irr  13326  decidr  13412  bj-charfunbi  13428  bj-omssind  13552  bj-om  13554  bj-inf2vnlem3  13589  bj-inf2vnlem4  13590