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-1 5  ax-2 6  ax-mp 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  342  dcbi  883  oplem1  922  3impexpbicom  1373  hband  1424  hb3and  1425  nfand  1506  nfimd  1523  equsexd  1665  euim  2017  mopick2  2032  2moswapdc  2039  necon3bd  2299  necon3d  2300  necon2ad  2313  necon1abiddc  2318  ralrimd  2452  rspcimedv  2725  2reuswapdc  2820  ra5  2928  difin  3237  r19.2m  3373  tpid3g  3561  sssnm  3604  ssiun  3778  ssiun2  3779  disjnim  3842  sotricim  4159  sotritrieq  4161  tron  4218  ordsucss  4334  ordunisuc2r  4344  ordpwsucss  4396  dmcosseq  4717  relssres  4763  trin2  4836  ssrnres  4886  fnun  5133  f1oun  5286  ssimaex  5378  chfnrn  5424  dffo4  5461  dffo5  5462  isoselem  5613  fnoprabg  5760  poxp  6011  issmo2  6068  smores  6071  tfr0dm  6101  tfrlemibxssdm  6106  tfr1onlembxssdm  6122  tfrcllembxssdm  6135  swoer  6334  qsss  6365  findcard  6658  findcard2  6659  findcard2s  6660  supmoti  6742  ctmlemr  6844  ctm  6845  pm54.43  6879  indpi  6962  recexprlemm  7244  recexprlemloc  7251  recexprlem1ssl  7253  recexprlem1ssu  7254  recexprlemss1l  7255  recexprlemss1u  7256  zmulcl  8864  indstr  9142  eluzdc  9158  icoshft  9468  fzouzsplit  9651  hashunlem  10273  modfsummod  10913  dvds2lem  11147  oddnn02np1  11219  dfgcd2  11342  sqrt2irr  11480  distop  11846  epttop  11851  decidr  11969  bj-omssind  12103  bj-om  12105  bj-inf2vnlem3  12140  bj-inf2vnlem4  12141