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  949  oplem1  988  3impexpbicom  1488  hband  1542  hb3and  1543  nfand  1621  nfimd  1638  equsexd  1782  euim  2155  mopick2  2170  2moswapdc  2177  necon3bd  2463  necon3d  2464  necon2ad  2477  necon1abiddc  2482  ralrimd  2628  rspcimedv  2931  2reuswapdc  3030  ra5  3141  difin  3468  r19.2m  3614  r19.2mOLD  3615  tpid3g  3826  sssnm  3877  ssiun  4052  ssiun2  4053  disjnim  4118  exmidsssnc  4338  sotricim  4466  sotritrieq  4468  tron  4525  ordsucss  4649  ordunisuc2r  4659  ordpwsucss  4712  dmcosseq  5052  relssres  5099  trin2  5177  ssrnres  5228  fnun  5487  f1oun  5657  ssimaex  5761  chfnrn  5814  dffo4  5850  dffo5  5851  isoselem  6020  fnoprabg  6183  poxp  6462  issmo2  6554  smores  6557  tfr0dm  6587  tfrlemibxssdm  6592  tfr1onlembxssdm  6608  tfrcllembxssdm  6621  swoer  6829  qsss  6862  findcard  7186  findcard2  7187  findcard2s  7188  supmoti  7327  ctmlemr  7442  ctm  7443  pm54.43  7530  indpi  7703  recexprlemm  7985  recexprlemloc  7992  recexprlem1ssl  7994  recexprlem1ssu  7995  recexprlemss1l  7996  recexprlemss1u  7997  zmulcl  9681  indstr  9976  eluzdc  9993  icoshft  10375  fzouzsplit  10571  seqf1oglem1  10939  seqf1oglem2  10940  hashunlem  11227  modfsummod  12208  dvds2lem  12553  oddnn02np1  12630  dfgcd2  12774  sqrt2irr  12923  ennnfonelemhom  13289  omctfn  13317  ptex  13601  kerf1ghm  14060  rmodislmodlem  14670  distop  15169  epttop  15174  restdis  15268  cnrest2  15320  cnptopresti  15322  uptx  15358  txcn  15359  logbgcd1irr  16052  gausslemma2dlem1a  16160  2sqlem10  16227  uhgrissubgr  16485  vtxdumgrfival  16522  decidr  16807  bj-charfunbi  16820  bj-omssind  16944  bj-om  16946  bj-inf2vnlem3  16981  bj-inf2vnlem4  16982