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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3828  sssnm  3879  ssiun  4054  ssiun2  4055  disjnim  4120  exmidsssnc  4342  sotricim  4470  sotritrieq  4472  tron  4529  ordsucss  4653  ordunisuc2r  4663  ordpwsucss  4716  dmcosseq  5056  relssres  5103  trin2  5182  ssrnres  5233  fnun  5492  f1oun  5662  ssimaex  5767  chfnrn  5823  dffo4  5859  dffo5  5860  isoselem  6029  fnoprabg  6192  poxp  6472  issmo2  6564  smores  6567  tfr0dm  6597  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  swoer  6839  qsss  6872  findcard  7197  findcard2  7198  findcard2s  7199  supmoti  7340  ctmlemr  7455  ctm  7456  pm54.43  7543  indpi  7716  recexprlemm  7998  recexprlemloc  8005  recexprlem1ssl  8007  recexprlem1ssu  8008  recexprlemss1l  8009  recexprlemss1u  8010  zmulcl  9710  indstr  10010  eluzdc  10027  icoshft  10410  fzouzsplit  10606  seqf1oglem1  10978  seqf1oglem2  10979  hashunlem  11267  fiidxsupcl  12019  modfsummod  12251  dvds2lem  12596  oddnn02np1  12673  dfgcd2  12817  sqrt2irr  12967  ennnfonelemhom  13365  omctfn  13393  ptex  13678  kerf1ghm  14137  rmodislmodlem  14797  distop  15323  epttop  15328  restdis  15422  cnrest2  15474  cnptopresti  15476  uptx  15512  txcn  15513  logbgcd1irr  16215  gausslemma2dlem1a  16394  2sqlem10  16461  uhgrissubgr  16719  vtxdumgrfival  16756  decidr  17041  bj-charfunbi  17054  bj-omssind  17178  bj-om  17180  bj-inf2vnlem3  17215  bj-inf2vnlem4  17216