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  944  oplem1  983  3impexpbicom  1483  hband  1537  hb3and  1538  nfand  1616  nfimd  1633  equsexd  1776  euim  2147  mopick2  2162  2moswapdc  2169  necon3bd  2444  necon3d  2445  necon2ad  2458  necon1abiddc  2463  ralrimd  2609  rspcimedv  2911  2reuswapdc  3009  ra5  3120  difin  3443  r19.2m  3580  r19.2mOLD  3581  tpid3g  3788  sssnm  3838  ssiun  4013  ssiun2  4014  disjnim  4079  exmidsssnc  4295  sotricim  4422  sotritrieq  4424  tron  4481  ordsucss  4604  ordunisuc2r  4614  ordpwsucss  4667  dmcosseq  5006  relssres  5053  trin2  5130  ssrnres  5181  fnun  5440  f1oun  5606  ssimaex  5710  chfnrn  5761  dffo4  5798  dffo5  5799  isoselem  5966  fnoprabg  6127  poxp  6402  issmo2  6460  smores  6463  tfr0dm  6493  tfrlemibxssdm  6498  tfr1onlembxssdm  6514  tfrcllembxssdm  6527  swoer  6735  qsss  6768  findcard  7082  findcard2  7083  findcard2s  7084  supmoti  7197  ctmlemr  7312  ctm  7313  pm54.43  7400  indpi  7567  recexprlemm  7849  recexprlemloc  7856  recexprlem1ssl  7858  recexprlem1ssu  7859  recexprlemss1l  7860  recexprlemss1u  7861  zmulcl  9538  indstr  9832  eluzdc  9849  icoshft  10230  fzouzsplit  10421  seqf1oglem1  10787  seqf1oglem2  10788  hashunlem  11073  modfsummod  12042  dvds2lem  12387  oddnn02np1  12464  dfgcd2  12608  sqrt2irr  12757  ennnfonelemhom  13059  omctfn  13087  ptex  13370  kerf1ghm  13884  rmodislmodlem  14388  distop  14838  epttop  14843  restdis  14937  cnrest2  14989  cnptopresti  14991  uptx  15027  txcn  15028  logbgcd1irr  15720  gausslemma2dlem1a  15816  2sqlem10  15883  uhgrissubgr  16141  vtxdumgrfival  16178  decidr  16453  bj-charfunbi  16466  bj-omssind  16590  bj-om  16592  bj-inf2vnlem3  16627  bj-inf2vnlem4  16628