Theorem imbitrrdi 162

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

Assertion

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

Proof of Theorem imbitrrdi

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

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr4g  205  imp4a  349  dcbi  938  oplem1  977  3impexpbicom  1449  hband  1500  hb3and  1501  nfand  1579  nfimd  1596  equsexd  1740  euim  2110  mopick2  2125  2moswapdc  2132  necon3bd  2407  necon3d  2408  necon2ad  2421  necon1abiddc  2426  ralrimd  2572  rspcimedv  2867  2reuswapdc  2965  ra5  3075  difin  3397  r19.2m  3534  r19.2mOLD  3535  tpid3g  3734  sssnm  3781  ssiun  3955  ssiun2  3956  disjnim  4021  exmidsssnc  4233  sotricim  4355  sotritrieq  4357  tron  4414  ordsucss  4537  ordunisuc2r  4547  ordpwsucss  4600  dmcosseq  4934  relssres  4981  trin2  5058  ssrnres  5109  fnun  5361  f1oun  5521  ssimaex  5619  chfnrn  5670  dffo4  5707  dffo5  5708  isoselem  5864  fnoprabg  6020  poxp  6287  issmo2  6344  smores  6347  tfr0dm  6377  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  swoer  6617  qsss  6650  findcard  6946  findcard2  6947  findcard2s  6948  supmoti  7054  ctmlemr  7169  ctm  7170  pm54.43  7252  indpi  7404  recexprlemm  7686  recexprlemloc  7693  recexprlem1ssl  7695  recexprlem1ssu  7696  recexprlemss1l  7697  recexprlemss1u  7698  zmulcl  9373  indstr  9661  eluzdc  9678  icoshft  10059  fzouzsplit  10249  seqf1oglem1  10593  seqf1oglem2  10594  hashunlem  10878  modfsummod  11604  dvds2lem  11949  oddnn02np1  12024  dfgcd2  12154  sqrt2irr  12303  ennnfonelemhom  12575  omctfn  12603  ptex  12878  kerf1ghm  13347  rmodislmodlem  13849  distop  14264  epttop  14269  restdis  14363  cnrest2  14415  cnptopresti  14417  uptx  14453  txcn  14454  logbgcd1irr  15140  gausslemma2dlem1a  15215  2sqlem10  15282  decidr  15358  bj-charfunbi  15373  bj-omssind  15497  bj-om  15499  bj-inf2vnlem3  15534  bj-inf2vnlem4  15535