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  945  oplem1  984  3impexpbicom  1484  hband  1538  hb3and  1539  nfand  1617  nfimd  1634  equsexd  1778  euim  2151  mopick2  2166  2moswapdc  2173  necon3bd  2457  necon3d  2458  necon2ad  2471  necon1abiddc  2476  ralrimd  2622  rspcimedv  2925  2reuswapdc  3023  ra5  3134  difin  3460  r19.2m  3598  r19.2mOLD  3599  tpid3g  3809  sssnm  3860  ssiun  4035  ssiun2  4036  disjnim  4101  exmidsssnc  4318  sotricim  4446  sotritrieq  4448  tron  4505  ordsucss  4628  ordunisuc2r  4638  ordpwsucss  4691  dmcosseq  5031  relssres  5078  trin2  5156  ssrnres  5207  fnun  5466  f1oun  5636  ssimaex  5740  chfnrn  5791  dffo4  5827  dffo5  5828  isoselem  5995  fnoprabg  6156  poxp  6430  issmo2  6522  smores  6525  tfr0dm  6555  tfrlemibxssdm  6560  tfr1onlembxssdm  6576  tfrcllembxssdm  6589  swoer  6797  qsss  6830  findcard  7147  findcard2  7148  findcard2s  7149  supmoti  7286  ctmlemr  7401  ctm  7402  pm54.43  7489  indpi  7662  recexprlemm  7944  recexprlemloc  7951  recexprlem1ssl  7953  recexprlem1ssu  7954  recexprlemss1l  7955  recexprlemss1u  7956  zmulcl  9636  indstr  9931  eluzdc  9948  icoshft  10329  fzouzsplit  10522  seqf1oglem1  10888  seqf1oglem2  10889  hashunlem  11176  modfsummod  12152  dvds2lem  12497  oddnn02np1  12574  dfgcd2  12718  sqrt2irr  12867  ennnfonelemhom  13187  omctfn  13215  ptex  13498  kerf1ghm  14012  rmodislmodlem  14547  distop  14999  epttop  15004  restdis  15098  cnrest2  15150  cnptopresti  15152  uptx  15188  txcn  15189  logbgcd1irr  15881  gausslemma2dlem1a  15980  2sqlem10  16047  uhgrissubgr  16305  vtxdumgrfival  16342  decidr  16617  bj-charfunbi  16630  bj-omssind  16754  bj-om  16756  bj-inf2vnlem3  16791  bj-inf2vnlem4  16792