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  1777  euim  2148  mopick2  2163  2moswapdc  2170  necon3bd  2445  necon3d  2446  necon2ad  2459  necon1abiddc  2464  ralrimd  2610  rspcimedv  2912  2reuswapdc  3010  ra5  3121  difin  3444  r19.2m  3581  r19.2mOLD  3582  tpid3g  3787  sssnm  3837  ssiun  4012  ssiun2  4013  disjnim  4078  exmidsssnc  4293  sotricim  4420  sotritrieq  4422  tron  4479  ordsucss  4602  ordunisuc2r  4612  ordpwsucss  4665  dmcosseq  5004  relssres  5051  trin2  5128  ssrnres  5179  fnun  5438  f1oun  5603  ssimaex  5707  chfnrn  5758  dffo4  5795  dffo5  5796  isoselem  5961  fnoprabg  6122  poxp  6397  issmo2  6455  smores  6458  tfr0dm  6488  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  swoer  6730  qsss  6763  findcard  7077  findcard2  7078  findcard2s  7079  supmoti  7192  ctmlemr  7307  ctm  7308  pm54.43  7395  indpi  7562  recexprlemm  7844  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  recexprlemss1u  7856  zmulcl  9533  indstr  9827  eluzdc  9844  icoshft  10225  fzouzsplit  10416  seqf1oglem1  10782  seqf1oglem2  10783  hashunlem  11068  modfsummod  12021  dvds2lem  12366  oddnn02np1  12443  dfgcd2  12587  sqrt2irr  12736  ennnfonelemhom  13038  omctfn  13066  ptex  13349  kerf1ghm  13863  rmodislmodlem  14367  distop  14812  epttop  14817  restdis  14911  cnrest2  14963  cnptopresti  14965  uptx  15001  txcn  15002  logbgcd1irr  15694  gausslemma2dlem1a  15790  2sqlem10  15857  uhgrissubgr  16115  vtxdumgrfival  16152  decidr  16413  bj-charfunbi  16427  bj-omssind  16551  bj-om  16553  bj-inf2vnlem3  16588  bj-inf2vnlem4  16589