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  937  oplem1  976  3impexpbicom  1448  hband  1499  hb3and  1500  nfand  1578  nfimd  1595  equsexd  1739  euim  2104  mopick2  2119  2moswapdc  2126  necon3bd  2400  necon3d  2401  necon2ad  2414  necon1abiddc  2419  ralrimd  2565  rspcimedv  2855  2reuswapdc  2953  ra5  3063  difin  3384  r19.2m  3521  r19.2mOLD  3522  tpid3g  3719  sssnm  3766  ssiun  3940  ssiun2  3941  disjnim  4006  exmidsssnc  4215  sotricim  4335  sotritrieq  4337  tron  4394  ordsucss  4515  ordunisuc2r  4525  ordpwsucss  4578  dmcosseq  4910  relssres  4957  trin2  5032  ssrnres  5083  fnun  5334  f1oun  5493  ssimaex  5590  chfnrn  5640  dffo4  5677  dffo5  5678  isoselem  5834  fnoprabg  5989  poxp  6246  issmo2  6303  smores  6306  tfr0dm  6336  tfrlemibxssdm  6341  tfr1onlembxssdm  6357  tfrcllembxssdm  6370  swoer  6576  qsss  6607  findcard  6901  findcard2  6902  findcard2s  6903  supmoti  7005  ctmlemr  7120  ctm  7121  pm54.43  7202  indpi  7354  recexprlemm  7636  recexprlemloc  7643  recexprlem1ssl  7645  recexprlem1ssu  7646  recexprlemss1l  7647  recexprlemss1u  7648  zmulcl  9319  indstr  9606  eluzdc  9623  icoshft  10003  fzouzsplit  10192  hashunlem  10797  modfsummod  11479  dvds2lem  11823  oddnn02np1  11898  dfgcd2  12028  sqrt2irr  12175  ennnfonelemhom  12429  omctfn  12457  ptex  12730  rmodislmodlem  13534  distop  13856  epttop  13861  restdis  13955  cnrest2  14007  cnptopresti  14009  uptx  14045  txcn  14046  logbgcd1irr  14656  2sqlem10  14743  decidr  14819  bj-charfunbi  14834  bj-omssind  14958  bj-om  14960  bj-inf2vnlem3  14995  bj-inf2vnlem4  14996