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  3024  ra5  3135  difin  3462  r19.2m  3600  r19.2mOLD  3601  tpid3g  3812  sssnm  3863  ssiun  4038  ssiun2  4039  disjnim  4104  exmidsssnc  4321  sotricim  4449  sotritrieq  4451  tron  4508  ordsucss  4631  ordunisuc2r  4641  ordpwsucss  4694  dmcosseq  5034  relssres  5081  trin2  5159  ssrnres  5210  fnun  5469  f1oun  5639  ssimaex  5743  chfnrn  5794  dffo4  5830  dffo5  5831  isoselem  5999  fnoprabg  6162  poxp  6441  issmo2  6533  smores  6536  tfr0dm  6566  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  swoer  6808  qsss  6841  findcard  7158  findcard2  7159  findcard2s  7160  supmoti  7297  ctmlemr  7412  ctm  7413  pm54.43  7500  indpi  7673  recexprlemm  7955  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  recexprlemss1u  7967  zmulcl  9651  indstr  9946  eluzdc  9963  icoshft  10345  fzouzsplit  10540  seqf1oglem1  10908  seqf1oglem2  10909  hashunlem  11196  modfsummod  12172  dvds2lem  12517  oddnn02np1  12594  dfgcd2  12738  sqrt2irr  12887  ennnfonelemhom  13253  omctfn  13281  ptex  13564  kerf1ghm  14030  rmodislmodlem  14627  distop  15079  epttop  15084  restdis  15178  cnrest2  15230  cnptopresti  15232  uptx  15268  txcn  15269  logbgcd1irr  15961  gausslemma2dlem1a  16060  2sqlem10  16127  uhgrissubgr  16385  vtxdumgrfival  16422  decidr  16707  bj-charfunbi  16720  bj-omssind  16844  bj-om  16846  bj-inf2vnlem3  16881  bj-inf2vnlem4  16882