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  2149  mopick2  2164  2moswapdc  2171  necon3bd  2455  necon3d  2456  necon2ad  2469  necon1abiddc  2474  ralrimd  2620  rspcimedv  2922  2reuswapdc  3020  ra5  3131  difin  3457  r19.2m  3595  r19.2mOLD  3596  tpid3g  3806  sssnm  3857  ssiun  4032  ssiun2  4033  disjnim  4098  exmidsssnc  4315  sotricim  4443  sotritrieq  4445  tron  4502  ordsucss  4625  ordunisuc2r  4635  ordpwsucss  4688  dmcosseq  5028  relssres  5075  trin2  5153  ssrnres  5204  fnun  5463  f1oun  5633  ssimaex  5737  chfnrn  5788  dffo4  5824  dffo5  5825  isoselem  5992  fnoprabg  6153  poxp  6427  issmo2  6519  smores  6522  tfr0dm  6552  tfrlemibxssdm  6557  tfr1onlembxssdm  6573  tfrcllembxssdm  6586  swoer  6794  qsss  6827  findcard  7144  findcard2  7145  findcard2s  7146  supmoti  7283  ctmlemr  7398  ctm  7399  pm54.43  7486  indpi  7653  recexprlemm  7935  recexprlemloc  7942  recexprlem1ssl  7944  recexprlem1ssu  7945  recexprlemss1l  7946  recexprlemss1u  7947  zmulcl  9627  indstr  9921  eluzdc  9938  icoshft  10319  fzouzsplit  10511  seqf1oglem1  10877  seqf1oglem2  10878  hashunlem  11163  modfsummod  12137  dvds2lem  12482  oddnn02np1  12559  dfgcd2  12703  sqrt2irr  12852  ennnfonelemhom  13155  omctfn  13183  ptex  13466  kerf1ghm  13980  rmodislmodlem  14485  distop  14937  epttop  14942  restdis  15036  cnrest2  15088  cnptopresti  15090  uptx  15126  txcn  15127  logbgcd1irr  15819  gausslemma2dlem1a  15918  2sqlem10  15985  uhgrissubgr  16243  vtxdumgrfival  16280  decidr  16555  bj-charfunbi  16568  bj-omssind  16692  bj-om  16694  bj-inf2vnlem3  16729  bj-inf2vnlem4  16730