Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl6ibr Unicode version

Theorem syl6ibr 161
 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
syl6ibr.1
syl6ibr.2
Assertion
Ref Expression
syl6ibr

Proof of Theorem syl6ibr
StepHypRef Expression
1 syl6ibr.1 . 2
2 syl6ibr.2 . . 3
32biimpri 132 . 2
41, 3syl6 33 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  3imtr4g  204  imp4a  347  dcbi  921  oplem1  960  3impexpbicom  1415  hband  1466  hb3and  1467  nfand  1548  nfimd  1565  equsexd  1708  euim  2068  mopick2  2083  2moswapdc  2090  necon3bd  2352  necon3d  2353  necon2ad  2366  necon1abiddc  2371  ralrimd  2513  rspcimedv  2795  2reuswapdc  2892  ra5  3001  difin  3318  r19.2m  3454  r19.2mOLD  3455  tpid3g  3646  sssnm  3689  ssiun  3863  ssiun2  3864  disjnim  3928  exmidsssnc  4134  sotricim  4253  sotritrieq  4255  tron  4312  ordsucss  4428  ordunisuc2r  4438  ordpwsucss  4490  dmcosseq  4818  relssres  4865  trin2  4938  ssrnres  4989  fnun  5237  f1oun  5395  ssimaex  5490  chfnrn  5539  dffo4  5576  dffo5  5577  isoselem  5729  fnoprabg  5880  poxp  6137  issmo2  6194  smores  6197  tfr0dm  6227  tfrlemibxssdm  6232  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  swoer  6465  qsss  6496  findcard  6790  findcard2  6791  findcard2s  6792  supmoti  6888  ctmlemr  7001  ctm  7002  pm54.43  7064  indpi  7175  recexprlemm  7457  recexprlemloc  7464  recexprlem1ssl  7466  recexprlem1ssu  7467  recexprlemss1l  7468  recexprlemss1u  7469  zmulcl  9132  indstr  9416  eluzdc  9432  icoshft  9804  fzouzsplit  9988  hashunlem  10583  modfsummod  11260  dvds2lem  11542  oddnn02np1  11614  dfgcd2  11739  sqrt2irr  11877  ennnfonelemhom  11965  omctfn  11993  distop  12294  epttop  12299  restdis  12393  cnrest2  12445  cnptopresti  12447  uptx  12483  txcn  12484  logbgcd1irr  13093  decidr  13175  bj-omssind  13305  bj-om  13307  bj-inf2vnlem3  13342  bj-inf2vnlem4  13343
 Copyright terms: Public domain W3C validator